diff --git a/.github/workflows/c6-tail-constant-certified.yml b/.github/workflows/c6-tail-constant-certified.yml new file mode 100644 index 000000000..3ac90f6b0 --- /dev/null +++ b/.github/workflows/c6-tail-constant-certified.yml @@ -0,0 +1,80 @@ +name: C6 tail constants certified enclosure + +'on': + pull_request: + paths: + - 'reviews/c6_tail_constant_certified_20260930/**' + - '.github/workflows/c6-tail-constant-certified.yml' + - 'frontiers/two_scale_cluster_geometry_20260929/RADIAL_TAIL.md' + - 'frontiers/extreme_cluster_sampling_20260930/PROOF.md' + - 'frontiers/radial_rate_20260930/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + certify-and-reject-mutants: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources and pins, replay both 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('reviews/c6_tail_constant_certified_20260930').resolve() + manifest_doc = json.loads((root / 'SOURCE_FILES.json').read_text()) + manifest = manifest_doc['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + # main-resident pins: the consumed sources must be the reviewed bytes + for pin in manifest_doc['pins_on_main']: + if not pin.get('workflow_checked'): + continue + p = pathlib.Path(pin['path']) + if p.is_symlink() or not p.is_file(): + raise ValueError('pinned source missing: ' + pin['path']) + data = p.read_bytes() + blob = hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + if blob != pin['git_blob']: + raise ValueError('pinned source drifted: ' + pin['path'] + ' ' + blob) + script = str(root / 'certify_tail_constants.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['gamma-power', 'cusp-shift', 'prefactor', 'pi-truncated', 'log2-truncated', 'tail-dropped', 'tb-power', 't2-weight', 't1t2-scale', 'j-scale', 'context-neg'] + def mutant_rc(args): + flags, m = args + return m, flags, subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=1500).returncode + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=1500).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + doc = json.loads(out) + if not (doc['passed'] and len(doc['checks']) == 12 and all(doc['checks'].values())): + raise RuntimeError('certification did not pass under ' + ' '.join(flags)) + with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool: + for m, fl, rc in pool.map(mutant_rc, [(flags, m) for m in mutants]): + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected under ' + ' '.join(fl)) + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False, 'certified_enclosures': True})) + PY + git diff --exit-code diff --git a/reviews/c6_tail_constant_certified_20260930/README.md b/reviews/c6_tail_constant_certified_20260930/README.md new file mode 100644 index 000000000..5f96b3d36 --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/README.md @@ -0,0 +1,260 @@ +# Certified enclosures of the planar microscopic radius-tail constants (parent kernel) + +**Object:** `C6-TAIL-CONSTANT-CERTIFIED-20260930-v1`. **Author lane:** Anthropic / Claude (session +`017Mi3hxjaxV45x6zo6o1ee3`; not the session that authored Math-#178). **Kind:** certified numerical record +(rigorous enclosures of stated integrals and of stated formulas). **Scientific effect:** NONE. **Register, catalog, +STATUS, GRAPH:** untouched; nothing here is a proposal to change them. **Same GitHub account as every lane: zero +organizational-independence credit.** Not a review of Math-#178 and not an acceptance of its planar reduction; the +reduction is consumed at that note's stated scope. The author will not merge. + +Claimed on Math-#178 in comment 5911696731 (this packet is that delivery, widened from `C_*(k, 0)` and `J_cusp` to +the complete table because the same run certifies it at no extra cost). + +## 1. What is certified + +Notation of Math-#178 `NOTE.md` §1–§2 (head `48407d4`), aligned planar cusp of the parent kernel `K(z) = exp(-|z|^2/2)`: + + A = a/(12k), gamma(a)^2 = 1 + A^2, + G_0(a) = exp(-a^2/4 - a^4/(576 k^2) - a^6/(248832 k^4)) = sqrt(192 pi^3) . p_odd(a, a^2/(12k), a^3/(144 k^2)), + +where `p_odd = N(0, diag(2, 2, 6))` is the exact contact regression of Math-#168 and `sqrt(192 pi^3) = (2 pi)^(3/2) 24^(1/2)` +its normalisation. The four raw one-dimensional integrals (all over the real line, all integrands even) + + J_hat(k) = int gamma^11 G_0 da, T_1(k) = int gamma^9 (1 + 12 A^2) G_0 da, + T_2(k) = int gamma^13 D_a G_0 da = -int gamma^13 [a^2/24 + a^4/(3456 k^2)] G_0 da, T_b(k) = int |A| gamma^10 G_0 da, + +are enclosed rigorously for `k in {1/2, 1, 2}`, and from them, with `p_b(0)/z_0 = phi(b/sqrt2)/(sqrt2 . 36 k^2 m_(2,b))`, +`m_(2,b) = (b^2 + 2) Phi(b/sqrt2) + b sqrt2 phi(b/sqrt2)`, `K_0 = 108 k^7 p_b(0)/z_0`, and the exact shape integrals +`I = 246528/35`, `U_2 = 240192/35`, `B = -428544/7`, `U_abs = 5898627/880`, `J = 1083417/280`, +`D = 27066286003/223205220 - (79298560/4782969) log 2`, `kappa = (2/13)(11/13)^(11/2)`, the constants of the table: + + J_cusp = J_hat/sqrt(192 pi^3), C_0 = (216/11) k^7 [p_b(0)/z_0] J_cusp, C_* = C_0 I ([R] (R12)-(R13) at d = 2), + G_max = C_0 (I - D), G_2 = C_0 J, B_2 = C_0 D, singleton = C_0 (I - D - J) ([E] E6, E20, E21), + C_2 = K_0 [U_2 T_1 + (2B/13) T_2] / sqrt(192 pi^3), c = C_2/C_*, kappa c, ([Q] (13), (16)), + B_sign = (K_0/C_*) U_abs T_b / sqrt(192 pi^3) ([Q] (19)), + +for `b in {0, 1}`. Every printed interval `[lo, hi]` in `RESULTS.json` is a rigorous enclosure of the exact real number +defined by the displayed formulas; no value is fitted, sampled, extrapolated or rounded outward by hand. + +Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than 40 digits (`D = 109.76995034568798474609191114...`). + +## 2. Method (every step is an enclosure) + +- **Arithmetic.** Intervals of `decimal` numbers at 48 digits with directed rounding (floor context for lower ends, + ceiling context for upper ends). `exp` and `sqrt` are correctly rounded by the `decimal` module and are widened by two + units in the last place on each side. Rationals enter through outward-rounded division. +- **Constants.** `pi` from Machin's formula with the alternating-series bracket (both arctangent series stopped at + consecutive partial sums); `log 2 = sum 1/(n 2^n)` to `N = 160` terms with the tail bound `1/((N + 1) 2^N)`; `erf(1/2)` + from its Maclaurin series with the alternating tail; `sqrt2`, `sqrt3` by interval `sqrt`. The widths of `pi`, `log 2`, + `erf(1/2)`, `kappa` and `D` are all below `1e-40` (rule `CONSTANTS_RIGOROUS`; the printed values carry 48 digits). +- **Cells.** `[0, T]` with `T = 16` is cut into `160` cells of width `1/10`. On a cell of centre `c` and half-width `r` + the integrand is expanded as a truncated Taylor series in `t = a - c` to order `K = 12` by Taylor-model arithmetic + (sum, product, scalar, integer power, `exp`, `sqrt` on truncated series with interval coefficients). The expansion at + the point `c` supplies the coefficients `p_0, ..., p_(K-1)`; the same recurrences evaluated with the whole cell in + place of `c` give an interval `[q_K]` that contains `f^(K)(xi)/K!` for every `xi` in the cell (inclusion monotonicity of + interval arithmetic applied to the exact coefficient recurrences). By Taylor's theorem with Lagrange remainder and + `K` even, `int_(-r)^(r) f(c + t) dt` lies in `sum_(j even < K) p_j 2 r^(j+1)/(j+1) + [q_K] 2 r^(K+1)/(K+1)`; odd terms + vanish by symmetry of the cell. The largest cell remainder width is printed (`max_cell_remainder_width`, at most + `8e-18` at `k = 1/2`, `3e-21` at `k = 1`, `7e-23` at `k = 2`). +- **Tail.** For `a >= T` every integrand is bounded by `(1 + s a^2)^7 (1 + a^2)^2 e^(-a^2/4)` with `s = 1/(144 k^2)` + (`gamma^15 a^2/24`, `gamma^9 (1 + 12 A^2)`, `gamma^11`, `A gamma^10` are all below it for `a >= 1`, `k >= 1/2`), and + `int_T^inf a^(2j) e^(-a^2/4) da <= (2/T) 4^j j! e^(-T^2/4) sum_(i <= j) (T^2/4)^i / i!`. The bound is `3.5e-18`, + `1.9e-21`, `1.9e-23` at `k = 1/2, 1, 2` and is added (for `T_2`, whose integrand is negative, subtracted) before doubling. +- **Rules (all twelve must hold; `passed` is `false` and the exit code `1` otherwise).** + `FLOAT_INSIDE` an independent 96-point Gauss-Legendre value on `[0, 14]` lies within `1e-11` relative of every raw + enclosure (the control is printed only to 10 significant digits, `float_reference_10sig`, so that the pinned output + does not depend on the interpreter's floating-point library); `NESTING` a coarser enclosure (a quarter of the cells, + order `K - 4`) contains the fine one; + `TRUNCATION_NESTING` the enclosure obtained by truncating at `T/2` (its own tail bound added) intersects the one at + `T`; `WIDTHS` every raw width is below `1e-11` relative; `PINNED` the printed leading digits of `J_hat(k)`, + `C_*(k, 0)`, `D`, `log 2`, `pi` begin both ends of the enclosures; `MONOTONE_IN_K` `J_hat(1/2) > J_hat(1) > J_hat(2)` + as disjoint intervals; `CONSTANTS_RIGOROUS` `pi`, `log 2`, `erf(1/2)`, `kappa`, `D` are bracketed below `1e-40` and + the pins hold; `TB_EXACT` and + `T2_IDENTITY` the two exact identities of section 3 hold as interval statements; `C_BOUNDS` the enclosure of `c(k)` + lies strictly inside the universal interval `(66451/11128, 199353/2782)` of section 3 at every `k`; `K_BOUNDS` the + enclosures of `J_hat(k)`, `I_9(k)`, `B_sign(k)` lie strictly inside the explicit all-`k` intervals of section 3 + (Consequence 3) and `c(k)` below its explicit all-`k` upper bound; `LIBRARY_EXACT` (v1.3) the decimal module's `exp` + and `sqrt`, and the interval negation, agree with exact rational brackets at six arguments (`e^-q` as `(e^(-q/64))^64` + from the rational series bracketed by consecutive partial sums, `sqrt q` from an integer square root; relative widths + below `1e-45`), which pins the two library primitives the enclosures rely on and detects an endpoint shortened to the + default 28-digit context. +- **Mutants (each must exit `1`, in both interpreter modes).** `gamma-power` (`gamma^10` in place of `gamma^11`), + `cusp-shift` (drops the `a^6` term of `G_0`), `prefactor` (`p_b(0)/z_0` scaled by `385/384`), `pi-truncated`, + `log2-truncated`, `tail-dropped` (no tail bound; caught only by `TRUNCATION_NESTING`), `tb-power` (`gamma^8` in the `T_b` + integrand on both evaluation paths; caught only by `TB_EXACT`), `t2-weight` (the `a^4` weight of `D_a G_0` scaled by + `1001/1000` on both paths; caught only by `T2_IDENTITY`), `t1t2-scale` (the `T_1` and `T_2` integrands both halved on + both paths, so `T_2 = -T_1/12` and the float control survive; caught only by `C_BOUNDS`), `j-scale` (the `J_hat` + integrand multiplied by `101/100` on both paths; caught by `K_BOUNDS` at every `k`, and by `PINNED`), `context-neg` + (v1.3: the interval negation of v1.2, `Iv(-a.hi, -a.lo)`, together with the default 28-digit current context; caught + only by `LIBRARY_EXACT`). + +Runtime about `30 s` per run (standard library only, `python -B -S certify_tail_constants.py`); the workflow runs the +script in both interpreter modes, compares the output byte for byte with `RESULTS.json`, and runs the eleven mutants +under each mode. + +## 3. Three exact identities (elementary; not used in `NOTE.md` at `48407d4`, which evaluates `T_1`, `T_2`, `T_b` separately) + +**(a) The cusp density is Gaussian in `gamma^6`.** Since `gamma^6 - 1 = 3A^2 + 3A^4 + A^6` and `A^2 = a^2/(144 k^2)`, + + G_0(a) = exp(-12 k^2 (gamma(a)^6 - 1)), G_0'(a) = -(a/2) gamma(a)^4 G_0(a). + +**(b) `T_b` is rational.** With `w = gamma^2`, `a da = 72 k^2 dw`, and then `v = w^3`: + + T_b(k) = 2 int_0^inf (a/(12k)) w^5 e^(-12 k^2 (w^3 - 1)) da = 12k int_1^inf w^5 e^(-12 k^2 (w^3 - 1)) dw + = 4k int_1^inf v e^(-12 k^2 (v - 1)) dv = 4k [1/(12 k^2) + 1/(144 k^4)] = (12 k^2 + 1)/(36 k^3), + +so `T_b(1/2) = 8/9`, `T_b(1) = 13/36`, `T_b(2) = 49/288`; the enclosures contain these rationals (`TB_EXACT`). Hence + + B_sign(k) = (11 U_abs/(2I)) . T_b(k)/J_hat(k) = (4587821/876544) . (12 k^2 + 1) / (36 k^3 J_hat(k)), + +with `11 U_abs/(2I) = 4587821/876544` the [Q]-corollary constant already displayed in Math-#178. + +**(c) `T_2 = -T_1/12`.** `a^2/24 + a^4/(3456 k^2) = (a^2/24) gamma^2`, so `T_2 = -(1/24) int a^2 gamma^15 G_0 da`. +By (a), `a^2 gamma^15 G_0 = -2 a gamma^11 G_0'`, and integrating by parts (boundary terms vanish), + + int a^2 gamma^15 G_0 da = 2 int (a gamma^11)' G_0 da = 2 int (12 gamma^11 - 11 gamma^9) G_0 da, + +because `(a gamma^11)' = gamma^11 + 11 A^2 gamma^9 = 12 gamma^11 - 11 gamma^9`. The same bracket is `T_1`: +`gamma^9 (1 + 12 A^2) = 12 gamma^11 - 11 gamma^9`. Therefore `T_2 = -T_1/12` (`T2_IDENTITY`: the enclosures of `T_2` and +of `-T_1/12` intersect at every `k`, at widths of `1e-16` to `1e-21`), and + + C_2 = K_0 T_1 (U_2 - B/78) / sqrt(192 pi^3), c(k) = (66451/11128) . T_1(k)/J_hat(k), + +with `11 (U_2 - B/78)/(2I) = 66451/11128 = 5.97151...`. `RESULTS.json` prints both evaluations (`c_reduced`, +`B_sign_reduced`) beside the assembled ones; they agree to the last digit. + +**Consequence 1 (two transcendental numbers per `k`).** Writing `I_p(k) = int gamma^p G_0 da`, the whole table depends +on `J_hat = I_11` and `T_1 = 12 I_11 - 11 I_9`; the family obeys `(1 + p) I_p - p I_(p-2) = 72 k^2 (I_(p+6) - I_(p+4))` +(from `int (a gamma^p G_0)' da = 0`), which does not relate `I_11` to `I_9` without lower members. + +**Consequence 2 (universal bounds on `c`, sharpening [Q]'s corollary).** Since `gamma > 1` off `a = 0` and `G_0 > 0`, +`0 < I_9 < I_11`, so `T_1/J_hat = 12 - 11 I_9/I_11` lies strictly in `(1, 12)` for every `k > 0`, and + + 66451/11128 = 5.97151... < c(k) = C_2/C_* < 12 . 66451/11128 = 199353/2782 = 71.658... + +at the scope of [Q] (13) (aligned planar cusp density of the parent kernel). Both ends are sharp as limits: with +`lambda = 12 k^2` and `I_p = 12k int (1 + A^2)^(p/2) exp(-lambda((1 + A^2)^3 - 1)) dA`, the mass sits at `A -> 0` when +`k -> inf` (`I_9/I_11 -> 1`, `c -> 66451/11128`) and at `A ~ lambda^(-1/6) -> inf` when `k -> 0` (`I_9/I_11 -> 0`, +`c -> 199353/2782`). The lower bound improves the author-side corollary `c > 4587/856 = 5.3586...` of [Q] +(Math-#176 comment 5903080058, quoted in Math-#178), which drops the `(2B/13) T_2` term instead of evaluating it; the +certified values `9.78`, `6.90`, `6.20` at `k = 1/2, 1, 2` sit inside, and `C_BOUNDS` checks the strict containment. +Nothing analogous sharpens `0 < B_sign < 4587821/876544`: `T_b/J_hat = int |A| gamma^10 G_0 / int gamma^11 G_0 < 1` +is [Q]'s bound and tends to `1` as `k -> 0` and to `0` as `k -> inf`. + +**Consequence 3 (explicit bounds for every `k > 0`).** Put `s = 4 sqrt3 . k . sqrt(gamma^6 - 1)` with the sign of `a` +(so `s^2/4 = 12 k^2 (gamma^6 - 1)`, `s` increases with `a`, and `s ~ a` near `0`). Then `ds/da = a gamma^4 / s` and + + J_hat(k) = int_R F(gamma) e^(-s^2/4) ds, F(gamma) = gamma^7 sqrt((gamma^4 + gamma^2 + 1)/3), + I_9(k) = int_R F_9(gamma) e^(-s^2/4) ds, F_9(gamma) = gamma^5 sqrt((gamma^4 + gamma^2 + 1)/3), + +with `gamma = gamma(s) = (1 + s^2/(48 k^2))^(1/6)`. Since `gamma >= 1`, `F >= F_9 >= 1` with equality only at `s = 0`, and +`gamma^4 + gamma^2 + 1 <= 3 gamma^4` gives `F <= gamma^9 = (1 + x)^(3/2)`, `F_9 <= gamma^7 = (1 + x)^(7/6)` with +`x = s^2/(48 k^2)`. Taylor's theorem (`(1 + x)^(3/2) <= 1 + (3/2) x + (3/8) x^2`, `(1 + x)^(7/6) <= 1 + (7/6) x + (7/72) x^2` +for `x >= 0`) and the Gaussian moments `int s^2 e^(-s^2/4) = 4 sqrt(pi)`, `int s^4 e^(-s^2/4) = 24 sqrt(pi)` give, for every +`k > 0`, + + 2 sqrt(pi) < J_hat(k) <= 2 sqrt(pi) (1 + 1/(16 k^2) + 1/(512 k^4)), + 2 sqrt(pi) < I_9(k) <= 2 sqrt(pi) (1 + 7/(144 k^2) + 7/(13824 k^4)), + +both lower bounds sharp as `k -> inf`. Consequently (exact `T_b`, Consequence 2, and `T_1/J_hat = 12 - 11 I_9/J_hat`): + + (4587821/876544) (12 k^2 + 1) / (36 k^3 . 2 sqrt(pi) (1 + 1/(16k^2) + 1/(512k^4))) < B_sign(k) < (4587821/876544) (12 k^2 + 1) / (72 sqrt(pi) k^3), + c(k) <= (66451/11128) [12 - 11 / (1 + 1/(16 k^2) + 1/(512 k^4))], + C_*(k, b) > (216/11) k^7 [p_b(0)/z_0] I . 2 sqrt(pi) / sqrt(192 pi^3) = (18 sqrt3 / (11 pi)) k^7 [p_b(0)/z_0] I, + +so `B_sign(k) = O(1/k)` explicitly (the universal `B_sign < 4587821/876544` of [Q] is beaten for `k > 0.31`) and +`c(k) -> 66451/11128` with an explicit rate. At `k = 1/2, 1, 2` the enclosures of `J_hat`, `I_9 = (12 J_hat - T_1)/11`, +`B_sign` and `c` satisfy these inequalities strictly (rule `K_BOUNDS`; the `J_hat` upper bound is within `0.7 %` at +`k = 1` and `0.2 %` at `k = 2`). Asymptotic remark (formal series in `1/k^2` from the same substitution, exact +coefficients, remainders not certified and not used): `J_hat/(2 sqrt(pi)) = 1 + 1/(18 k^2) + 13/(10368 k^4) +- 35/(746496 k^6) + O(k^-8)`, `I_9/(2 sqrt(pi)) = 1 + 1/(24 k^2) + 1/(10368 k^4) + 0 . k^-6 + O(k^-8)`, hence +`c(k)/(66451/11128) = 1 + 11/(72 k^2) + O(k^-4)`; the certified values give `(J_hat/(2 sqrt pi) - 1 - 1/(18k^2)) k^4 = +0.00112, 0.00121, 0.00124` at `k = 1/2, 1, 2` against `13/10368 = 0.001254`. + +## 4. Certified values + +Raw integrals (`RESULTS.json` → `raw_integrals`; the bracket shows the digits at which the two ends differ; `w` is the width): + +| `k` | `J_hat` | `T_1` | `T_2` | `T_b` | +|---|---|---|---|---| +| `1/2` | `4.396080052560476[29…33]` (w `4.3e-17`) | `7.2017156701259[6993…7017]` (w `2.3e-16`) | `-0.600142972510497[601…413]` (w `1.9e-16`) | `0.888888888888888[876…908]` (w `3.2e-17`) = `8/9` | +| `1` | `3.74614172836573455` (w `4.5e-20`) | `4.33121953848605581` (w `1.5e-19`) | `-0.360934961540504651` (w `1.4e-19`) | `0.361111111111111111` (w `2.4e-20`) = `13/36` | +| `2` | `3.59441780573178758` (w `1.5e-21`) | `3.73260661394902763` (w `2.9e-21`) | `-0.311050551162418969` (w `3.9e-21`) | `0.170138888888888889` (w `4.7e-22`) = `49/288` | + +Normalised cusp integral and the `b`-free constants (`RESULTS.json` → `constants`, identical for `b = 0` and `b = 1`): + +| `k` | `J_cusp = J_hat/sqrt(192 pi^3)` | `c = C_2/C_*` | `kappa c` | `B_sign` | +|---|---|---|---|---| +| `1/2` | `0.05697576550737183` | `9.782610960502025` | `0.600499647330249[7…8]` | `1.058314213529843` | +| `1` | `0.04855218515605283` | `6.904152846784694` | `0.4238072398409664` | `0.5045327835799602` | +| `2` | `0.04658575448725384` | `6.201090480499020` | `0.3806501824142391` | `0.2477466432952960` | + +Tail constants (`F(t) ~ C_* t^(-11)` is the `r^(-3)`-scaled expected number of near points at scaled radius `> t`; the split +columns are [E]'s whole-cluster decomposition): + +| `k` | `b` | `C_*` | `G_max` | `G_2` | `B_2` | singleton | +|---|---|---|---|---|---|---| +| `1/2` | `0` | `1.929709931071402` | `1.899636893866561` | `1.060062419071862` | `0.03007303720484126` | `0.8395744747946980` | +| `1/2` | `1` | `0.5524932519127913` | `0.5438830717750065` | `0.3035053733792919` | `0.00861018013778482[5…6]` | `0.2403776983957146` | +| `1` | `0` | `52.62118476458856` | `51.80112428725574` | `28.90680071538336` | `0.8200604773328205` | `22.89432357187237` | +| `1` | `1` | `15.06591691423265` | `14.83112624824110` | `8.276276176269632` | `0.2347906659915518` | `6.554850071971470` | +| `2` | `0` | `1615.678527435135` | `1590.499426843761` | `887.5531294407690` | `25.17910059137386` | `702.9462974029917` | +| `2` | `1` | `462.5832459558805` | `455.3742437416235` | `254.1144173196261` | `7.209002214256986` | `201.2598264219975` | + +All sixteen digits shown are common to both ends of the enclosure unless a bracket says otherwise; the full intervals +(up to 48 digits) are in `RESULTS.json`. The universal ratios `(I - D)/I`, `J/I`, `D/I` and the bounds of [Q]'s +corollary (`c > 4587/856`, `0 < B_sign < 4587821/876544`) hold inside every enclosure. + +## 5. Comparison with Math-#178 + +Every number in Math-#178 `RESULTS.json` (blob `0b5ce76f`, `per_k` cusp values and the complete `table`, 78 values, plus +`D_inner` and `kappa`) lies within `9e-16` relative of the corresponding certified enclosure, that is, at the rounding +level of its own floating-point arithmetic; 96-point Gauss-Legendre on `[0, 14]` was, for these integrands, accurate to +the last printed digit. The certification shares no code with `tail_constants.py` (different method, different +quadrature, different arithmetic) and does not consume its numbers except in this comparison. The near-mass identity +(N) of that note (a four-dimensional integral) is **not** certified here. + +## 6. Exposure, disposition, non-claims + +- **Exposure.** This session authored none of [R], [E], [Q], Math-#168 or Math-#178; it posted nonauthor reads of [E] + Slices A, B, C (Math-#169) and of Math-#181/#185 slices. Same GitHub account and same provider as Math-#178's author: + zero organizational-independence credit; a Claude read of a Claude packet counts for nothing towards acceptance. +- **What this record is.** A certified evaluation of formulas taken from merged sources ([R] (R12)-(R13); [E] E6, E20, + E21; [Q] (12), (13), (16), (19), (21)-(22); all pinned on `main` by blob and checked by the workflow) through the planar + reduction of Math-#178 §1, which is consumed at that note's stated scope and is not reviewed here. The three + identities of section 3 are elementary calculus on the displayed integrands and change no formula of any source. +- **What it is not.** Not a proof of any theorem; not a review of Math-#178 (its Slice A/B/C read requests stand with + the non-Claude lanes); no register, catalog, STATUS, PROOF_INDEX or GRAPH change. Catalog **C8** (numerical constants: + finite `C`, `r_*`, `z_*`, `c_(B,K)`, `c_(d,L)` on a declared band) stays **OPEN**: the constants certified here are the + limiting microscopic tail coefficients of the `r -> 0`-first law, a different object; this record is information for the + integrators, not a C8 candidate. Planar (`d = 2`), parent kernel, aligned frame; no rate in `r`, no finite-`r` statement, + nothing on the remote singleton population; `k in {1/2, 1, 2}` and `b in {0, 1}` only (any other `k`, `b` is a one-line + change of the constants `KS`, `BS` and a rerun). + +## 7. Files and reproduction + +`certify_tail_constants.py` (standard library; `--mutant NAME`; `--T`, `--cells`, `--K` for experiments, the pinned run is +the default), `RESULTS.json` (the script's stdout, byte-identical in `-B -S` and `-B -O -S`), `SOURCE_FILES.json` +(manifest, the three `main` pins with blobs, the Math-#178 companion at head `48407d4`), workflow +`.github/workflows/c6-tail-constant-certified.yml` (manifest and pin verification, both modes against `RESULTS.json`, +the eleven mutants under each mode in parallel, clean tree; triggered by changes to the packet, the workflow or any of +the three pinned sources). The workflow pins CPython 3.11.16; the pinned output is byte-identical under other CPython 3.x +versions as well, since the only floating-point quantity it prints is rounded to 10 significant digits (everything else +is `decimal`/`fractions` arithmetic). + + python -B -S reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py | diff - reviews/c6_tail_constant_certified_20260930/RESULTS.json + python -B -S reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py --mutant tail-dropped; echo $? # 1 + +## 8. Revisions + +- **v1.3 (30 September 2026, rigor repair, values unchanged).** The interval class negated endpoints with the Decimal + unary minus, `Iv(-a.hi, -a.lo)`, which rounds its operand to the thread's *current* context (default precision 28), not + to the 48-digit contexts every other step names. In this script the operation is never applied to an endpoint longer + than 28 digits, and the repaired script reproduces every one of the 167 intervals of v1.2 byte for byte; the defect was + found in a sibling packet (`frontiers/c8_window_coefficient_planar_20260930`), where `exp(-x)` at a 60-digit `x` went + wrong beyond the 28th digit. Repair: negation is the exact `copy_negate`, the two-ulp widening of `exp` and `sqrt` + goes through the ceiling context, the current context is widened to `2 . 48 + 20` digits as a safety net, and rule + `LIBRARY_EXACT` with mutant `context-neg` (which reinstates the v1.2 negation and the 28-digit current context) are + added. Twelve rules, eleven mutants; `RESULTS.json` differs from v1.2 only by the new rule's entry. +- v1.2: all-`k` bounds (section 3, Consequence 3), rule `K_BOUNDS`, mutant `j-scale`. v1.1: Codex findings (float + reference rounded to ten digits, `log 2` series length, trigger paths). v1.0: initial record. diff --git a/reviews/c6_tail_constant_certified_20260930/RESULTS.json b/reviews/c6_tail_constant_certified_20260930/RESULTS.json new file mode 100644 index 000000000..2735dc391 --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/RESULTS.json @@ -0,0 +1,917 @@ +{ + "D_inner": [ + "109.769950345687984746091911144322714480157052373", + "109.769950345687984746091911144322714480157052375" + ], + "cells": 160, + "checks": { + "CONSTANTS_RIGOROUS": true, + "C_BOUNDS": true, + "FLOAT_INSIDE": true, + "K_BOUNDS": true, + "LIBRARY_EXACT": true, + "MONOTONE_IN_K": true, + "NESTING": true, + "PINNED": true, + "T2_IDENTITY": true, + "TB_EXACT": true, + "TRUNCATION_NESTING": true, + "WIDTHS": true + }, + "constants": { + "k=1,b=0": { + "B2": [ + "0.820060477332820453427583913757754509621126819120", + "0.820060477332820453437420585881481923303985092503" + ], + "B_sign": [ + "0.504532783579960197454103040229546843535934710651", + "0.504532783579960197493704475658357833862002197892" + ], + "B_sign_reduced": [ + "0.504532783579960197468255136514829456633366543616", + "0.504532783579960197474307035984352842456248076637" + ], + "C0_per_shape": [ + "0.00747071921550736411208111600285851339885204344343", + "0.00747071921550736411217072770526659252130534591740" + ], + "C2": [ + "363.304702593617453981073967146739559663615232082", + "363.304702593617454007609646274276563897648604548" + ], + "C_star": [ + "52.6211847645885559949466675986486740340627590291", + "52.6211847645885559955778617063989291740675519522" + ], + "C_star_width": "6.311941077502551400047929231E-19", + "G2": [ + "28.9068007153833639436378087731034357537288726833", + "28.9068007153833639439845474937743423916252641351" + ], + "G_max": [ + "51.8011242872557355415190836848909195244416322099", + "51.8011242872557355421404411205174472507635668597" + ], + "J_cusp": [ + "0.0485521851560528317659531596156492181850366540727", + "0.0485521851560528317665355458413870143147268658487" + ], + "K0": [ + "0.846284375321634430422119177341158878766075943917", + "0.846284375321634430422119177341158878766075944080" + ], + "T1": [ + "0.0561351353558714362152271669459178879289182392004", + "0.0561351353558714362172340561405747487398878468426" + ], + "T2": [ + "-0.00467792794632261968564160825014655347419132113455", + "-0.00467792794632261968377476282247528896534902035656" + ], + "Tb": [ + "0.00468021094765769600011083515377536426280387187061", + "0.00468021094765769600042205161105164046170690917479" + ], + "c_C2_over_Cstar": [ + "6.90415284678469413544945233293146410680079213287", + "6.90415284678469413603654553240318088938539430274" + ], + "c_reduced": [ + "6.90415284678469413557479770314195170055027098858", + "6.90415284678469413590444402048071741124628869226" + ], + "dTV_coefficient_kappa_c": [ + "0.423807239840966445757592039196701251167500880905", + "0.423807239840966445793630399574743081596795358924" + ], + "singleton": [ + "22.8943235718723715978812749117874837707127595265", + "22.8943235718723715981558936267431048591383027248" + ] + }, + "k=1,b=1": { + "B2": [ + "0.234790665991551752188175905327811484317163131482", + "0.234790665991551752190992232736470589653074155705" + ], + "B_sign": [ + "0.504532783579960197454103040229546843535934710619", + "0.504532783579960197493704475658357833862002197924" + ], + "B_sign_reduced": [ + "0.504532783579960197468255136514829456633366543616", + "0.504532783579960197474307035984352842456248076637" + ], + "C0_per_shape": [ + "0.00213893388174220730813466331749522267052609828142", + "0.00213893388174220730816031995120772700648021648819" + ], + "C2": [ + "104.017393152821051339670417253533875895200517755", + "104.017393152821051347267820063575605442567724905" + ], + "C_star": [ + "15.0659169142326538074234936667274929862702273463", + "15.0659169142326538076042101980382435272444231544" + ], + "C_star_width": "1.807165313107505409741958081E-19", + "G2": [ + "8.27627617626963219699047331232400592869062079200", + "8.27627617626963219708974771634864989349920252497" + ], + "G_max": [ + "14.8311262482411020552353177613996815019530642148", + "14.8311262482411020554132179653017729375913489987" + ], + "J_cusp": [ + "0.0485521851560528317659531596156492181850366540727", + "0.0485521851560528317665355458413870143147268658487" + ], + "K0": [ + "0.242298803066653454271694697802036188389345544710", + "0.242298803066653454271694697802036188389345544769" + ], + "T1": [ + "0.0561351353558714362152271669459178879289182392004", + "0.0561351353558714362172340561405747487398878468426" + ], + "T2": [ + "-0.00467792794632261968564160825014655347419132113455", + "-0.00467792794632261968377476282247528896534902035656" + ], + "Tb": [ + "0.00468021094765769600011083515377536426280387187061", + "0.00468021094765769600042205161105164046170690917479" + ], + "c_C2_over_Cstar": [ + "6.90415284678469413544945233293146410680079213244", + "6.90415284678469413603654553240318088938539430315" + ], + "c_reduced": [ + "6.90415284678469413557479770314195170055027098858", + "6.90415284678469413590444402048071741124628869226" + ], + "dTV_coefficient_kappa_c": [ + "0.423807239840966445757592039196701251167500880878", + "0.423807239840966445793630399574743081596795358949" + ], + "singleton": [ + "6.55485007197146985824484444907567557326244342282", + "6.55485007197146985832347024895312304409214647367" + ] + }, + "k=1/2,b=0": { + "B2": [ + "0.0300730372048412614003608893447232850057061231747", + "0.0300730372048412616976612059478598301276255260783" + ], + "B_sign": [ + "1.05831421352984302111038636415859780503065954361", + "1.05831421352984306972662066296448280849658878869" + ], + "B_sign_reduced": [ + "1.05831421352984303602562861965335419777094873311", + "1.05831421352984304648806208139131304851428020440" + ], + "C0_per_shape": [ + "0.000273964205232261902287971736489955663362032369778", + "0.000273964205232261904996366116435260822205465323985" + ], + "C2": [ + "18.8776015222887014705822410391921347137155174576", + "18.8776015222887026269232047628401265320905245348" + ], + "C_star": [ + "1.92970993107140177849283132152559399363757474447", + "1.92970993107140179756983274150148514219054158262" + ], + "C_star_width": "1.907700141997589114855296683815E-17", + "G2": [ + "1.06006241907186247639688383868835105333108222845", + "1.06006241907186248687659995989264633646920937471" + ], + "G_max": [ + "1.89963689386656051709247043218087070863186862129", + "1.89963689386656053587217153555362531206291605654" + ], + "J_cusp": [ + "0.0569757655073718298483949476989128256181921250274", + "0.0569757655073718304116540893901560022850536386775" + ], + "K0": [ + "0.0264463867288010759506912242919112149614398732474", + "0.0264463867288010759506912242919112149614398732526" + ], + "T1": [ + "0.0933384420588227398240609425840399030597776605102", + "0.0933384420588227428475819200661507221896957907803" + ], + "T2": [ + "-0.00777820350490189637249596844041314243923515498667", + "-0.00777820350490189393319610080932126730043534542650" + ], + "Tb": [ + "0.0115205192557727899920788779442785700444719774333", + "0.0115205192557727904074107251452197834278023931215" + ], + "c_C2_over_Cstar": [ + "9.78261096050202452063560864973096480207256327402", + "9.78261096050202521657639502615005373095083477803" + ], + "c_reduced": [ + "9.78261096050202465644594367326080710306296469072", + "9.78261096050202507004531478261554033880797582926" + ], + "dTV_coefficient_kappa_c": [ + "0.600499647330249745760627912753305844312132774275", + "0.600499647330249788480531471131129824099919074838" + ], + "singleton": [ + "0.839574474794698040695586593492519655300786392840", + "0.839574474794698048995571575660978975593706681836" + ] + }, + "k=1/2,b=1": { + "B2": [ + "0.00861018013778482542350275775963941130153890469838", + "0.00861018013778482550862250351519547133455110378639" + ], + "B_sign": [ + "1.05831421352984302111038636415859780503065954357", + "1.05831421352984306972662066296448280849658878873" + ], + "B_sign_reduced": [ + "1.05831421352984303602562861965335419777094873311", + "1.05831421352984304648806208139131304851428020440" + ], + "C0_per_shape": [ + "0.0000784384078763779183467396341588356138864230045960", + "0.0000784384078763779191221772242050787089553398005752" + ], + "C2": [ + "5.40482654176547833614495026457669062720106246968", + "5.40482654176547866721573405483240435842071722758" + ], + "C_star": [ + "0.552493251912791298691000815140269320576916870772", + "0.552493251912791304152917335109418398895486010178" + ], + "C_star_width": "5.461916519969149078318569139406E-18", + "G2": [ + "0.303505373379291911290962907933797158178524115608", + "0.303505373379291914291399577559263427215240645429" + ], + "G_max": [ + "0.543883071775006473267498057380629909275377966073", + "0.543883071775006478644294831594222927560934906392" + ], + "J_cusp": [ + "0.0569757655073718298483949476989128256181921250274", + "0.0569757655073718304116540893901560022850536386775" + ], + "K0": [ + "0.00757183759583292044599045930631363088716704827224", + "0.00757183759583292044599045930631363088716704827400" + ], + "T1": [ + "0.0933384420588227398240609425840399030597776605102", + "0.0933384420588227428475819200661507221896957907803" + ], + "T2": [ + "-0.00777820350490189637249596844041314243923515498667", + "-0.00777820350490189393319610080932126730043534542650" + ], + "Tb": [ + "0.0115205192557727899920788779442785700444719774333", + "0.0115205192557727904074107251452197834278023931215" + ], + "c_C2_over_Cstar": [ + "9.78261096050202452063560864973096480207256327380", + "9.78261096050202521657639502615005373095083477833" + ], + "c_reduced": [ + "9.78261096050202465644594367326080710306296469072", + "9.78261096050202507004531478261554033880797582926" + ], + "dTV_coefficient_kappa_c": [ + "0.600499647330249745760627912753305844312132774261", + "0.600499647330249788480531471131129824099919074857" + ], + "singleton": [ + "0.240377698395714561976535149446832751096853850464", + "0.240377698395714564352895254034959500345694260964" + ] + }, + "k=2,b=0": { + "B2": [ + "25.1791005913738603498149535940917787667120214764", + "25.1791005913738603498257873479838752423120304875" + ], + "B_sign": [ + "0.247746643295296011750602312428032120528047229641", + "0.247746643295296011751390613487070314077239554835" + ], + "B_sign_reduced": [ + "0.247746643295296011750916151761598256918865316186", + "0.247746643295296011751022749141886485890291358313" + ], + "C0_per_shape": [ + "0.229380632058953583504141944226192279148287082085", + "0.229380632058953583504240639304927204077448259087" + ], + "C2": [ + "10018.9687360246879184199613009761927306343067057", + "10018.9687360246879184397556544394340310323398244" + ], + "C_star": [ + "1615.67852743513454383168872074842086268196907920", + "1615.67852743513454383238389504471696476586184047" + ], + "C_star_width": "6.9517429629610208389276127E-19", + "G2": [ + "887.553129440768980640381974241816287492856234325", + "887.553129440768980640763859692236845214202716128" + ], + "G_max": [ + "1590.49942684376068348187376715432908391525705772", + "1590.49942684376068348255810769673308952354980998" + ], + "J_cusp": [ + "0.0465857544872538436674809505145367473878549108631", + "0.0465857544872538436675009948603290447707027127252" + ], + "K0": [ + "27.0811000102923017735078136749170841205144302052", + "27.0811000102923017735078136749170841205144302107" + ], + "T1": [ + "0.0483767621665027267401004550607324010090366281451", + "0.0483767621665027267401380742293190373233448487143" + ], + "T2": [ + "-0.00403139684720856056170192332117391075073199099064", + "-0.00403139684720856056165172850825712160512466400238" + ], + "Tb": [ + "0.00220509938880026061549589525490241203552976230739", + "0.00220509938880026061550196284211715666395862456373" + ], + "c_C2_over_Cstar": [ + "6.20109048049902023666907462134201722310500687677", + "6.20109048049902023668399416861888627685516350732" + ], + "c_reduced": [ + "6.20109048049902023667275444253051382861916242323", + "6.20109048049902023668024471871607707131908679576" + ], + "dTV_coefficient_kappa_c": [ + "0.380650182414239118963463492111689792208471476529", + "0.380650182414239118964379319482752607829251307347" + ], + "singleton": [ + "702.946297402991702841491792912512796422400823401", + "702.946297402991702841794248004496244309347093852" + ] + }, + "k=2,b=1": { + "B2": [ + "7.20900221425698565807093095780436937518222052396", + "7.20900221425698565807403275866152927296015488846" + ], + "B_sign": [ + "0.247746643295296011750602312428032120528047229636", + "0.247746643295296011751390613487070314077239554842" + ], + "B_sign_reduced": [ + "0.247746643295296011750916151761598256918865316186", + "0.247746643295296011751022749141886485890291358313" + ], + "C0_per_shape": [ + "0.0656737312129081398353939460508067211759016842850", + "0.0656737312129081398354222033365884100042346475124" + ], + "C2": [ + "2868.52056293534753984324886483699812353059770702", + "2868.52056293534753984891616567756821504637123791" + ], + "C_star": [ + "462.583245955880511352571392343236553087219726382", + "462.583245955880511352770426976070501186398833770" + ], + "C_star_width": "1.99034632833948099179107388E-19", + "G2": [ + "254.114417319626064771582153030453090843685268153", + "254.114417319626064771691490258273590719849603944" + ], + "G_max": [ + "455.374243741623525694500461385432183712037505858", + "455.374243741623525694696394217408971913438678882" + ], + "J_cusp": [ + "0.0465857544872538436674809505145367473878549108631", + "0.0465857544872538436675009948603290447707027127252" + ], + "K0": [ + "7.75356169813291053669423032966515802845905743080", + "7.75356169813291053669423032966515802845905743259" + ], + "T1": [ + "0.0483767621665027267401004550607324010090366281451", + "0.0483767621665027267401380742293190373233448487143" + ], + "T2": [ + "-0.00403139684720856056170192332117391075073199099064", + "-0.00403139684720856056165172850825712160512466400238" + ], + "Tb": [ + "0.00220509938880026061549589525490241203552976230739", + "0.00220509938880026061550196284211715666395862456373" + ], + "c_C2_over_Cstar": [ + "6.20109048049902023666907462134201722310500687665", + "6.20109048049902023668399416861888627685516350748" + ], + "c_reduced": [ + "6.20109048049902023667275444253051382861916242323", + "6.20109048049902023668024471871607707131908679576" + ], + "dTV_coefficient_kappa_c": [ + "0.380650182414239118963463492111689792208471476522", + "0.380650182414239118964379319482752607829251307357" + ], + "singleton": [ + "201.259826421997460922918308354979092868352237704", + "201.259826421997460923004903959135381193589074940" + ] + } + }, + "erf_half": [ + "0.520499877813046537682746653891964528736451575728", + "0.520499877813046537682746653891964528736451575795" + ], + "exact_relations": { + "B_sign_prefactor": "4587821/876544", + "G0": "exp(-12 k^2 (gamma^6 - 1))", + "T2": "-T1/12", + "Tb": "(12 k^2 + 1)/(36 k^3)", + "c_bounds": { + "lower": "66451/11128", + "note": "T1/J_hat = 12 - 11 I_9/I_11 with 0 < I_9 < I_11; both ends are limits (k -> inf, k -> 0)", + "upper": "199353/2782" + }, + "c_prefactor": "66451/11128", + "k_dependent_bounds": { + "B_sign": "B_PREF (12k^2+1)/(36 k^3) / upJ < B_sign(k) < B_PREF (12k^2+1)/(72 sqrt(pi) k^3)", + "I_9": "2 sqrt(pi) < I_9(k) <= 2 sqrt(pi) (1 + 7/(144 k^2) + 7/(13824 k^4))", + "J_hat": "2 sqrt(pi) < J_hat(k) <= 2 sqrt(pi) (1 + 1/(16 k^2) + 1/(512 k^4))", + "asymptotic_series_not_certified": { + "I_9/(2 sqrt pi)": "1 + 1/(24 k^2) + 1/(10368 k^4) + 0 k^-6 + O(k^-8)", + "J_hat/(2 sqrt pi)": "1 + 1/(18 k^2) + 13/(10368 k^4) - 35/(746496 k^6) + O(k^-8)", + "c/C_PREF": "1 + 11/(72 k^2) + O(k^-4)" + }, + "c": "c(k) <= C_PREF (12 - 11 . 2 sqrt(pi)/upJ)", + "per_k": { + "1": { + "B_sign": [ + "0.504532783579960197468255136514829456633366543616", + "0.504532783579960197474307035984352842456248076637" + ], + "B_sign_bounds": [ + [ + "0.500889723853113662357150381608132469494509236053", + "0.500889723853113662357150381608132469494509236123" + ], + [ + "0.533173631835833878876263589797719132567397526659", + "0.533173631835833878876263589797719132567397526732" + ] + ], + "I_9": [ + "3.69295283653661443597774312994838083993967317872", + "3.69295283653661443604084020104104412586778966340" + ], + "I_9_bounds": [ + [ + "3.54490770181103205459633496668229036559509891200", + "3.54490770181103205459633496668229036559509891244" + ], + [ + "3.71902462379668676850482103745610945979642068291", + "3.71902462379668676850482103745610945979642068342" + ] + ], + "J_hat": [ + "3.74614172836573455033513841998214633256472187646", + "3.74614172836573455038007360333691238118122447828" + ], + "J_hat_bounds": [ + [ + "3.54490770181103205459633496668229036559509891200", + "3.54490770181103205459633496668229036559509891244" + ], + [ + "3.77338808102932122999023936883173486181509552156", + "3.77338808102932122999023936883173486181509552204" + ] + ], + "c": [ + "6.90415284678469413557479770314195170055027098858", + "6.90415284678469413590444402048071741124628869226" + ], + "c_upper": [ + "9.94886986459480671947447219675634320236909621363", + "9.94886986459480671947447219675634320236909622978" + ] + }, + "1/2": { + "B_sign": [ + "1.05831421352984303602562861965335419777094873311", + "1.05831421352984304648806208139131304851428020440" + ], + "B_sign_bounds": [ + [ + "1.02433358161330936579604862280087127907882751838", + "1.02433358161330936579604862280087127907882751853" + ], + [ + "1.31242740144205262492618729796361632631974775793", + "1.31242740144205262492618729796361632631974775811" + ] + ], + "I_9": [ + "4.14102226914543139206762980275322692333761755445", + "4.14102226914543146068568362261892910699383579748" + ], + "I_9_bounds": [ + [ + "3.54490770181103205459633496668229036559509891200", + "3.54490770181103205459633496668229036559509891244" + ], + [ + "4.26291562752507211195091670183205982621910621475", + "4.26291562752507211195091670183205982621910621533" + ] + ], + "J_hat": [ + "4.39608005256047628984657690235788762705235688108", + "4.39608005256047633330597152674136876691298772436" + ], + "J_hat_bounds": [ + [ + "3.54490770181103205459633496668229036559509891200", + "3.54490770181103205459633496668229036559509891244" + ], + [ + "4.54191299294538481995155417606168453091872048100", + "4.54191299294538481995155417606168453091872048157" + ] + ], + "c": [ + "9.78261096050202465644594367326080710306296469072", + "9.78261096050202507004531478261554033880797582926" + ], + "c_upper": [ + "20.3905332187757535375497536427556942715365327564", + "20.3905332187757535375497536427556942715365327694" + ] + }, + "2": { + "B_sign": [ + "0.247746643295296011750916151761598256918865316186", + "0.247746643295296011751022749141886485890291358313" + ], + "B_sign_bounds": [ + [ + "0.247312362151320576359122903882580266755121317682", + "0.247312362151320576359122903882580266755121317716" + ], + [ + "0.251206807307267885239778037500848437459639219291", + "0.251206807307267885239778037500848437459639219326" + ] + ], + "I_9": [ + "3.58185518680294757048843990497576233746754826875", + "3.58185518680294757049039093458566189257243186192" + ], + "I_9_bounds": [ + [ + "3.54490770181103205459633496668229036559509891200", + "3.54490770181103205459633496668229036559509891244" + ], + [ + "3.58810036609226727679657152418739368471076185129", + "3.58810036609226727679657152418739368471076185178" + ] + ], + "J_hat": [ + "3.59441780573178757508336100029782500857967171872", + "3.59441780573178757508490756220742747016140332740" + ], + "J_hat_bounds": [ + [ + "3.54490770181103205459633496668229036559509891200", + "3.54490770181103205459633496668229036559509891244" + ], + [ + "3.60072961264277315994825479220743873683066626547", + "3.60072961264277315994825479220743873683066626592" + ] + ], + "c": [ + "6.20109048049902023667275444253051382861916242323", + "6.20109048049902023668024471871607707131908679576" + ], + "c_upper": [ + "6.98984972237704037777492284555261125070424140620", + "6.98984972237704037777492284555261125070424142294" + ] + } + } + }, + "per_k": { + "1": { + "T2_enclosure": [ + "-0.360934961540504650756162793462443870156345266422", + "-0.360934961540504650612122570874516774947553040520" + ], + "Tb_enclosure": [ + "0.361111111111111111100981979010184105434315929778", + "0.361111111111111111124994512192976729559760014656" + ], + "Tb_exact": "13/36", + "minus_T1_over_12": [ + "-0.360934961540504650688873884196130562620021462624", + "-0.360934961540504650675970085715955265802417286846" + ] + }, + "1/2": { + "T2_enclosure": [ + "-0.600142972510497601373032699862262101370897738080", + "-0.600142972510497413163933711644056007251692398162" + ], + "Tb_enclosure": [ + "0.888888888888888876361424978359559634087704282170", + "0.888888888888888908407190970514898421028490976696" + ], + "Tb_exact": "8/9", + "minus_T1_over_12": [ + "-0.600142972510497513784582916500762947326207456158", + "-0.600142972510497494344094872674017085501971576686" + ] + }, + "2": { + "T2_enclosure": [ + "-0.311050551162418968804123602699942006633239403652", + "-0.311050551162418968800250720715110201707467156868" + ], + "Tb_enclosure": [ + "0.170138888888888888888673361143316460152471457000", + "0.170138888888888888889141518067306514606320109713" + ], + "Tb_exact": "49/288", + "minus_T1_over_12": [ + "-0.311050551162418968802291087403376199234419139022", + "-0.311050551162418968802049205503904068636674120644" + ] + } + } + }, + "kappa": [ + "0.0613843941821676280477188642920775402962871118467", + "0.0613843941821676280477188642920775402962871118476" + ], + "log2": [ + "0.693147180559945309417232121458176568075500134360", + "0.693147180559945309417232121458176568075500134361" + ], + "object": "C6-TAIL-CONSTANT-CERTIFIED-20260930-v1", + "passed": true, + "pi": [ + "3.14159265358979323846264338327950288419716939901", + "3.14159265358979323846264338327950288419716939965" + ], + "precision_digits": 48, + "raw_integrals": { + "J|1": { + "coarse_enclosure": [ + "3.74614170556060146635079886442350330546718213384", + "3.74614175116806672453737990767164057712568224422" + ], + "enclosure_at_half_T": [ + "3.74614172830673384075315554254170651708102059456", + "3.75027725260702018231699243816832075691318839936" + ], + "float_reference_10sig": "3.746141728", + "interval": [ + "3.74614172836573455033513841998214633256472187646", + "3.74614172836573455038007360333691238118122447828" + ], + "max_cell_remainder_width": "8.16502808602988998693472605690989427699903284704E-22", + "tail_bound_at_T": "1.87713873585565334886175595787939884103799358980E-21", + "width": "4.493518335476604861650260182E-20" + }, + "J|1/2": { + "coarse_enclosure": [ + "4.39607724977892103555740737202715835129944842344", + "4.39608285570652085616494105794446160317152043832" + ], + "enclosure_at_half_T": [ + "4.39608005256047628984657685915077717227612500764", + "4.88338636508862619334623971076851614454862582206" + ], + "float_reference_10sig": "4.396080053", + "interval": [ + "4.39608005256047628984657690235788762705235688108", + "4.39608005256047633330597152674136876691298772436" + ], + "max_cell_remainder_width": "1.20153198092803751893957263577931451146324352974E-18", + "tail_bound_at_T": "3.49542098081589710467854089486196880544602412155E-18", + "width": "4.345939462438348113986063084328E-17" + }, + "J|2": { + "coarse_enclosure": [ + "3.59441780277745773977363400065554754806368072798", + "3.59441780867806450577199778610904541721136791144" + ], + "enclosure_at_half_T": [ + "3.59441779293996319066325662486836917181403587930", + "3.59500855337833238063115278410442542179757241854" + ], + "float_reference_10sig": "3.594417806", + "interval": [ + "3.59441780573178757508336100029782500857967171872", + "3.59441780573178757508490756220742747016140332740" + ], + "max_cell_remainder_width": "2.51594557359301231703110684485527745086687223406E-23", + "tail_bound_at_T": "1.85613966008643238499823688796721641135862006274E-23", + "width": "1.54656190960246158173160868E-21" + }, + "T1|1": { + "coarse_enclosure": [ + "4.33121946663301935787764512381933820822290190364", + "4.33121961034752536579818638400942353234295511976" + ], + "enclosure_at_half_T": [ + "4.33121953822329624601780335004655369058166078410", + "4.33535506252358258769153318608467375891175381196" + ], + "float_reference_10sig": "4.331219538", + "interval": [ + "4.33121953848605580811164102859146318962900744216", + "4.33121953848605580826648661035356675144025755148" + ], + "max_cell_remainder_width": "3.03888078896464608876735661683774747977416691921E-21", + "tail_bound_at_T": "1.87713873585565334886175595787939884103799358980E-21", + "width": "1.5484558176210356181125010932E-19" + }, + "T1|1/2": { + "coarse_enclosure": [ + "7.20169963378670025717917408781246118395063674574", + "7.20173170786053427200261968081719548724617032974" + ], + "enclosure_at_half_T": [ + "7.20171567012596993212913812382198594393315933852", + "7.68902198265412002545526287697702991717020433876" + ], + "float_reference_10sig": "7.20171567", + "interval": [ + "7.20171567012596993212913847208820502602365892024", + "7.20171567012597016541499499800915536791448947388" + ], + "max_cell_remainder_width": "7.55790121883335246205076398749400324904041576541E-18", + "tail_bound_at_T": "3.49542098081589710467854089486196880544602412155E-18", + "width": "2.3328585652592095034189083055364E-16" + }, + "T1|2": { + "coarse_enclosure": [ + "3.73260660902472351736744595654569432514134390186", + "3.73260661886814860572255819448353246233153093744" + ], + "enclosure_at_half_T": [ + "3.73260658646099722786050074527686975310092239614", + "3.73319734689936641782975153808620982806073412484" + ], + "float_reference_10sig": "3.732606614", + "interval": [ + "3.73260661394902762562459046604684882364008944774", + "3.73260661394902762562749304884051439081302966826" + ], + "max_cell_remainder_width": "4.77703128713435777447946155988680556554094456175E-23", + "tail_bound_at_T": "1.85613966008643238499823688796721641135862006274E-23", + "width": "2.90258279366556717294022052E-21" + }, + "T2|1": { + "coarse_enclosure": [ + "-0.360935014116756499825769152289227429048983849460", + "-0.360934908966916388491717265922916415464025138638" + ], + "enclosure_at_half_T": [ + "-0.365070485496240399550346221915389782079150339902", + "-0.360934961195954057887438364740434401523191902062" + ], + "float_reference_10sig": "-0.3609349615", + "interval": [ + "-0.360934961540504650756162793462443870156345266422", + "-0.360934961540504650612122570874516774947553040520" + ], + "max_cell_remainder_width": "2.87275550704400139109519215738555160241854956481E-21", + "tail_bound_at_T": "1.87713873585565334886175595787939884103799358980E-21", + "width": "1.44040222587927095208792225902E-19" + }, + "T2|1/2": { + "coarse_enclosure": [ + "-0.600153087597411225982230013779628157255025857132", + "-0.600132858152240299752915452807291895456170224126" + ], + "enclosure_at_half_T": [ + "-1.08744928503864746141330002138713933112874928731", + "-0.600142972510497413163932805935240337465407677130" + ], + "float_reference_10sig": "-0.6001429725", + "interval": [ + "-0.600142972510497601373032699862262101370897738080", + "-0.600142972510497413163933711644056007251692398162" + ], + "max_cell_remainder_width": "6.23325763933023250572994151913800648297281274594E-18", + "tail_bound_at_T": "3.49542098081589710467854089486196880544602412155E-18", + "width": "1.88209098988218206094119205339918E-16" + }, + "T2|2": { + "coarse_enclosure": [ + "-0.311050556381409119387856513329229838723580826200", + "-0.311050545949421850398761367134265295978094044768" + ], + "enclosure_at_half_T": [ + "-0.311641266924490796780306586134670095950311265966", + "-0.311050506486121606810088168415933590451284075044" + ], + "float_reference_10sig": "-0.3110505512", + "interval": [ + "-0.311050551162418968804123602699942006633239403652", + "-0.311050551162418968800250720715110201707467156868" + ], + "max_cell_remainder_width": "6.44615667963908069007745031918274522770197475073E-23", + "tail_bound_at_T": "1.85613966008643238499823688796721641135862006274E-23", + "width": "3.872881984831804925772246784E-21" + }, + "Tb|1": { + "coarse_enclosure": [ + "0.361111101048457261673231469611678325118772680572", + "0.361111121172622860749709830732261607703721994684" + ], + "enclosure_at_half_T": [ + "0.361111111078053558425933873185099410625468084994", + "0.365246635378339899968849781659484400185135045946" + ], + "float_reference_10sig": "0.3611111111", + "interval": [ + "0.361111111111111111100981979010184105434315929778", + "0.361111111111111111124994512192976729559760014656" + ], + "max_cell_remainder_width": "4.05990206455714911283517243040637346340648165472E-22", + "tail_bound_at_T": "1.87713873585565334886175595787939884103799358980E-21", + "width": "2.4012533182792624125444084878E-20" + }, + "Tb|1/2": { + "coarse_enclosure": [ + "0.888887059251897962854048851126497454992965541966", + "0.888890718704923715469847752075036418549299484972" + ], + "enclosure_at_half_T": [ + "0.888888888888888876361424943743882319520634723480", + "1.37619520141703876844745916313348311268771294836" + ], + "float_reference_10sig": "0.8888888889", + "interval": [ + "0.888888888888888876361424978359559634087704282170", + "0.888888888888888908407190970514898421028490976696" + ], + "max_cell_remainder_width": "8.32749357040578418891000359394695098274066717169E-19", + "tail_bound_at_T": "3.49542098081589710467854089486196880544602412155E-18", + "width": "3.2045765992155338786940786694526E-17" + }, + "Tb|2": { + "coarse_enclosure": [ + "0.170138888160451458786155904795231368937057571930", + "0.170138889615458306056469401087422110580011023831" + ], + "enclosure_at_half_T": [ + "0.170138884755738839737704086392721482615205220531", + "0.170729645194108029704522357987856065959794837027" + ], + "float_reference_10sig": "0.1701388889", + "interval": [ + "0.170138888888888888888673361143316460152471457000", + "0.170138888888888888889141518067306514606320109713" + ], + "max_cell_remainder_width": "7.21831120564129082013051829697546711877993618170E-24", + "tail_bound_at_T": "1.85613966008643238499823688796721641135862006274E-23", + "width": "4.68156923990054453848652713E-22" + } + }, + "scope": "rigorous enclosures of the one-dimensional cusp integrals and of the assembled constants; the planar reductions and the exact shape integrals are consumed at their records' scopes; not a proof of any theorem; scientific effect NONE", + "taylor_order": 12, + "truncation": 16 +} diff --git a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json new file mode 100644 index 000000000..725fc903e --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json @@ -0,0 +1,77 @@ +{ + "schema": 1, + "object": "C6-TAIL-CONSTANT-CERTIFIED-20260930-v1", + "scientific_effect": "NONE", + "certified": true, + "review_status": "SUPPORT_RECORD_FOR_MATH_178_NOT_A_REVIEW", + "disposition": "CERTIFIED_ENCLOSURES_OF_STATED_FORMULAS_NO_REGISTER_CHANGE", + "declarative": true, + "executed": false, + "base": "fa2e9909d8cca40d38b7dc2eadda6766bd0788e1", + "pins_on_main": [ + { + "label": "R", + "path": "frontiers/two_scale_cluster_geometry_20260929/RADIAL_TAIL.md", + "git_blob": "0f14417ef7038b9c6f50e4b01e393a58b7b5e3a4", + "role": "(R12) J_cusp and (R13) C_* = (216/11) k^7 (c_m/z_0) I J_cusp: the object whose planar value is enclosed", + "workflow_checked": true + }, + { + "label": "E", + "path": "frontiers/extreme_cluster_sampling_20260930/PROOF.md", + "git_blob": "19a6044f2066643b5baab34ce5b6b6efb431e84a", + "role": "E20 J = 1083417/280, E21 D = 27066286003/223205220 - (79298560/4782969) log 2, E6 whole-cluster split G_max, G_2, B_2 (Math-#169, merged)", + "workflow_checked": true + }, + { + "label": "Q", + "path": "frontiers/radial_rate_20260930/PROOF.md", + "git_blob": "65f24b1f9a7b80522a2ee059f5f6877c9f970f0d", + "role": "(12) U_abs, (13) C_2 with T_1 and T_2, (16) kappa, (19) B_sign, (21)-(22) the aligned planar cusp density and D_a G_0 (Math-#176, merged)", + "workflow_checked": true + } + ], + "unmerged_companion": { + "label": "NOTE", + "pr": 178, + "head": "48407d43d2603b8f04f8ba3824b53fac903ed0be", + "files": [ + { + "path": "frontiers/c6_microscopic_tail_numerics_20260930/NOTE.md", + "git_blob": "674cb9772dde7fe5ddbf35c6fe11c1d462795c6a", + "role": "section 1 planar reduction (p_b(0)/z_0, p_odd = N(0, diag(2, 2, 6)), the one-dimensional cusp integrals) and section 2 assembly; consumed at its stated scope, not reviewed here" + }, + { + "path": "frontiers/c6_microscopic_tail_numerics_20260930/RESULTS.json", + "git_blob": "0b5ce76f5f950f3ef09fc0e26dafa884a43d8f63", + "role": "the floating-point table compared against the enclosures in README section 5" + }, + { + "path": "frontiers/c6_microscopic_tail_numerics_20260930/tail_constants.py", + "git_blob": "ff1f5d4b61859367ffcbebe9e1b5bf7990b2ef0b", + "role": "the Gauss-Legendre evaluator; no code shared with certify_tail_constants.py" + } + ], + "workflow_checked": false + }, + "files": [ + { + "path": "README.md", + "bytes": 21599, + "sha256": "f207c320cbe3a676f8a683d5c26a0b74cf66d74d7fec708bf7a6b3517e70b799", + "git_blob": "5f96b3d36defbcd7e32fbb4e9b1d0053aa55d047" + }, + { + "path": "RESULTS.json", + "bytes": 35072, + "sha256": "c595d223a0f6f9df297443469024094225d0da8f388e1d7c2ed9dbbc59f3e8ec", + "git_blob": "2735dc391818bb431ea7fa3842dde44d1748ea04" + }, + { + "path": "certify_tail_constants.py", + "bytes": 27779, + "sha256": "2edbc5a7407673a7abeb6f4f7d2f548f417c43a384182c937493a7379d48816c", + "git_blob": "aa590e2b2deea620d88324dc6dcb1ee1dfeb6f2b" + } + ] +} diff --git a/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py new file mode 100644 index 000000000..aa590e2b2 --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py @@ -0,0 +1,564 @@ +"""Certified enclosures of the planar microscopic radius-tail constants (Math-#178's table) for the parent kernel. + +Standard library only. Run from anywhere: python -B -S certify_tail_constants.py [--mutant NAME] +Every printed interval [lo, hi] is a rigorous enclosure: interval arithmetic over `decimal` with directed rounding +(exp and sqrt are correctly rounded by the decimal module and widened by two units in the last place), pi from Machin's +formula with the alternating-series bracket, log 2 and erf(1/2) from their series with explicit tails, and every +one-dimensional integral enclosed cell by cell with order-K Taylor arithmetic: the point expansion at the cell centre +supplies the even coefficients, and the K-th coefficient of the expansion over the whole cell (which contains +f^(K)(xi)/K! for every xi in the cell) supplies the remainder; beyond the truncation point T an exact Gaussian tail bound +is added. Nothing is fitted, sampled or extrapolated. + +Inputs certified (from Math-#178 NOTE section 1-2 at head 48407d4, planar reduction of [R] (R12)-(R13) and [Q]): + G0(a) = p_odd(a, a^2/(12k), a^3/(144 k^2)), p_odd = N(0, diag(2, 2, 6)), gamma(a) = sqrt(1 + (a/(12k))^2), A = a/(12k) + J_cusp = int gamma^11 G0, T1 = int gamma^9 (1 + 12 A^2) G0, T2 = int gamma^13 D_a G0, Tb = int |A| gamma^10 G0, + D_a G0 = -(a^2/24 + a^4/(3456 k^2)) G0; all integrals over the real line (even integrands). + p_b(0)/z_0 = phi(b/sqrt2) / (sqrt2 . 36 k^2 m_(2,b)), m_(2,b) = (b^2 + 2) Phi(b/sqrt2) + b sqrt2 phi(b/sqrt2) + K_0 = 108 k^7 p_b(0)/z_0; C_0 = (216/11) k^7 [p_b(0)/z_0] J_cusp; C_* = C_0 I; C_2 = K_0 [U_2 T1 + (2B/13) T2]; + c = C_2/C_*; d_TV coefficient kappa c with kappa = (2/13)(11/13)^(11/2); B_sign = (K_0/C_*) U_abs Tb; + G_max = C_0 (I - D), G_2 = C_0 J, B_2 = C_0 D, singleton = C_0 (I - D - J); + I = 246528/35, U_2 = 240192/35, B = -428544/7, U_abs = 5898627/880, J = 1083417/280 (exact, Math-#169/#176/#178), + D = 27066286003/223205220 - (79298560/4782969) log 2 (Math-#169 E21). +The reductions are consumed at those records' stated scopes; this script certifies the arithmetic of the constants, not +the theorems. Scientific effect: NONE. + +Twelve rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, +TB_EXACT, T2_IDENTITY, C_BOUNDS, K_BOUNDS, LIBRARY_EXACT; README section 2) and eleven mutants must exit 1. The floating-point control enters the +pinned output only rounded to 10 significant digits, so the output is byte-identical across CPython versions. TB_EXACT and T2_IDENTITY are the exact +identities of README section 3: G_0 = exp(-12 k^2 (gamma^6 - 1)), Tb(k) = (12 k^2 + 1)/(36 k^3), T2 = -T1/12, whence +c = (66451/11128) T1/J_hat and B_sign = (4587821/876544) Tb/J_hat; C_BOUNDS is their consequence +66451/11128 < c(k) < 199353/2782 (T1/J_hat = 12 - 11 I_9/I_11 with 0 < I_9 < I_11); K_BOUNDS the all-k two-sided +bounds 2 sqrt(pi) < J_hat(k) <= 2 sqrt(pi)(1 + 1/(16k^2) + 1/(512k^4)) and their consequences for I_9, B_sign and c. +""" +import argparse +import json +import math +import sys +import time +from decimal import Decimal, Context, ROUND_FLOOR, ROUND_CEILING, ROUND_HALF_EVEN, setcontext +from fractions import Fraction as Fr +from math import comb, factorial + +MUTANTS = ("gamma-power", "cusp-shift", "prefactor", "pi-truncated", "log2-truncated", "tail-dropped", "tb-power", "t2-weight", + "t1t2-scale", "j-scale", "context-neg") +MUT = None + + +def T2_WEIGHT(): + """Coefficient multiplier of the a^4 term of D_a G0 (mutant t2-weight perturbs it on both evaluation paths).""" + return Fr(1001, 1000) if MUT == "t2-weight" else Fr(1) + + +def T1T2_SCALE(): + """Common factor on the T1 and T2 integrands, both evaluation paths (mutant t1t2-scale halves them: T2 = -T1/12 + survives, the float control survives, only the universal bounds on c catch it).""" + return Fr(1, 2) if MUT == "t1t2-scale" else Fr(1) + + +def J_SCALE(): + """Factor on the J integrand, both evaluation paths (mutant j-scale multiplies it by 101/100, which leaves the + float control and the identities intact and is caught by the all-k bounds K_BOUNDS, as well as by PINNED).""" + return Fr(101, 100) if MUT == "j-scale" else Fr(1) + + +def TB_POWER(): + """Power of gamma^2 in the Tb integrand (mutant tb-power lowers it on both evaluation paths).""" + return 4 if MUT == "tb-power" else 5 +PREC = 48 +CF = Context(prec=PREC, rounding=ROUND_FLOOR, Emin=-9999999, Emax=9999999) +CC = Context(prec=PREC, rounding=ROUND_CEILING, Emin=-9999999, Emax=9999999) +CE = Context(prec=PREC, rounding=ROUND_HALF_EVEN, Emin=-9999999, Emax=9999999) +# Every arithmetic step names one of the three contexts. Operator syntax on Decimals (unary minus, int * Decimal) rounds to +# the thread's current context, whose default precision is 28 and would silently shorten a 48-digit endpoint (v1.2 negated +# endpoints that way; repaired in v1.3). The current context is widened as a safety net, negation is the exact copy_negate, +# and rule LIBRARY_EXACT compares exp, sqrt and the negation against exact rational brackets. +setcontext(Context(prec=2 * PREC + 20, rounding=ROUND_HALF_EVEN, Emin=-9999999, Emax=9999999)) +ZERO, ONE = Decimal(0), Decimal(1) +KS = (Fr(1, 2), Fr(1), Fr(2)) +BS = (Fr(0), Fr(1)) +I_SHAPE, U2, BSH, UABS, JOUT = Fr(246528, 35), Fr(240192, 35), Fr(-428544, 7), Fr(5898627, 880), Fr(1083417, 280) +# exact prefactors of the two reduced formulas (README section 3): c = C_PREF . T1/J_hat, B_sign = B_PREF . Tb/J_hat +C_PREF = Fr(11) * (U2 - BSH / 78) / (2 * I_SHAPE) +B_PREF = Fr(11) * UABS / (2 * I_SHAPE) +# universal bounds (README section 3, consequence): T1/J_hat = 12 - 11 I_9/I_11 lies strictly in (1, 12) for every k > 0 +C_LOWER, C_UPPER = C_PREF, 12 * C_PREF # 66451/11128 < c(k) < 199353/2782 +# first significant digits of the certified values (pinned by this record; PINNED check): key -> string prefix +PINNED = { + "J_hat|1/2": "4.396080052560", "J_hat|1": "3.746141728365734", "J_hat|2": "3.594417805731787", + "C_star|1/2|0": "1.929709931071", "C_star|1|0": "52.6211847645885", "C_star|2|0": "1615.67852743513", + "D": "109.76995034568", "log2": "0.69314718055994530941", "pi": "3.14159265358979323846", +} + + +def ulp(x): + if x == 0: + return Decimal(1).scaleb(-PREC - 30) + return Decimal(1).scaleb(x.adjusted() - PREC + 1) + + +class Iv: + """Closed interval [lo, hi] of Decimals; every operation encloses the exact result.""" + __slots__ = ("lo", "hi") + + def __init__(self, lo, hi=None): + if hi is None: + hi = lo + if lo > hi: + raise ValueError("empty interval") + self.lo, self.hi = lo, hi + + @staticmethod + def frac(q): + q = Fr(q) + n, d = Decimal(q.numerator), Decimal(q.denominator) + return Iv(CF.divide(n, d), CC.divide(n, d)) + + @staticmethod + def of(x): + return x if isinstance(x, Iv) else Iv.frac(x) + + def __add__(a, b): + b = Iv.of(b) + return Iv(CF.add(a.lo, b.lo), CC.add(a.hi, b.hi)) + __radd__ = __add__ + + def __neg__(a): + if MUT == "context-neg": # v1.2 behaviour: rounds to the current context + return Iv(-a.hi, -a.lo) + return Iv(a.hi.copy_negate(), a.lo.copy_negate()) # exact + + def __sub__(a, b): + b = Iv.of(b) + return Iv(CF.subtract(a.lo, b.hi), CC.subtract(a.hi, b.lo)) + + def __rsub__(a, b): + return Iv.of(b) - a + + def __mul__(a, b): + b = Iv.of(b) + c = [(x, y) for x in (a.lo, a.hi) for y in (b.lo, b.hi)] + return Iv(min(CF.multiply(x, y) for x, y in c), max(CC.multiply(x, y) for x, y in c)) + __rmul__ = __mul__ + + def __truediv__(a, b): + b = Iv.of(b) + if b.lo <= 0 <= b.hi: + raise ZeroDivisionError("interval division by an interval containing 0") + c = [(x, y) for x in (a.lo, a.hi) for y in (b.lo, b.hi)] + return Iv(min(CF.divide(x, y) for x, y in c), max(CC.divide(x, y) for x, y in c)) + + def __rtruediv__(a, b): + return Iv.of(b) / a + + def exp(a): + lo, hi = CE.exp(a.lo), CE.exp(a.hi) + return Iv(max(ZERO, CF.subtract(lo, CC.multiply(Decimal(2), ulp(lo)))), CC.add(hi, CC.multiply(Decimal(2), ulp(hi)))) + + def sqrt(a): + if a.lo < 0: + raise ValueError("sqrt of an interval with negative part") + lo, hi = CE.sqrt(a.lo), CE.sqrt(a.hi) + return Iv(max(ZERO, CF.subtract(lo, CC.multiply(Decimal(2), ulp(lo)))), CC.add(hi, CC.multiply(Decimal(2), ulp(hi)))) + + def width(a): + return CC.subtract(a.hi, a.lo) + + def contains(a, x): + x = Iv.of(x) + return a.lo <= x.lo and x.hi <= a.hi + + def intersects(a, b): + return a.lo <= b.hi and b.lo <= a.hi + + def mid_float(a): + return float((a.lo + a.hi) / 2) + + def pair(a): + return [str(a.lo), str(a.hi)] + + +# ---------------- rigorous constants +def pi_interval(): + def atan_inv(n, terms): + x = Fr(1, n) + partial, sums = Iv(ZERO), [] + for m in range(terms + 2): + t = Iv.frac(x ** (2 * m + 1) / (2 * m + 1)) + partial = partial + t if m % 2 == 0 else partial - t + sums.append(partial) + a, b = sums[-1], sums[-2] # alternating series with decreasing terms + return Iv(min(a.lo, b.lo), max(a.hi, b.hi)) + if MUT == "pi-truncated": + return Iv.frac(Fr(314159, 100000)) + return atan_inv(5, 40) * 16 - atan_inv(239, 20) * 4 + + +def log2_interval(): + # log 2 = sum_{n>=1} 1/(n 2^n); tail after N terms <= 1/((N+1) 2^N); N = 160 puts the tail below 1e-50 + N = 160 if MUT != "log2-truncated" else 8 + s = sum(Fr(1, n * 2 ** n) for n in range(1, N + 1)) + lo = Iv.frac(s) + hi = Iv.frac(s + Fr(1, (N + 1) * 2 ** N)) + return Iv(lo.lo, hi.hi) + + +def erf_interval(x): + """erf(x) for rational 0 <= x <= 1: (2/sqrt pi) sum (-1)^n x^(2n+1)/(n! (2n+1)), alternating with decreasing terms.""" + x = Fr(x) + partial, sums = Fr(0), [] + for n in range(60): + t = x ** (2 * n + 1) / (factorial(n) * (2 * n + 1)) + partial = partial + t if n % 2 == 0 else partial - t + sums.append(partial) + S = Iv(Iv.frac(min(sums[-1], sums[-2])).lo, Iv.frac(max(sums[-1], sums[-2])).hi) + return S * 2 / pi_interval().sqrt() + + +def library_exact(): + """exp and sqrt of the decimal module, and the interval negation, against exact rational brackets: e^-q by the rational + series of e^(-q/64) raised to the 64th power (alternating, bracketed by consecutive partial sums), sqrt by an integer root. + Catches an argument shortened to the default 28-digit context (mutant context-neg) at the 1e-28 level.""" + ok = True + for q in (Fr(48) - Fr(51035039649098175696, 10 ** 29), Fr(3), Fr(1, 2), Fr(288), Fr(5, 7), Fr(1234567, 10 ** 6)): + g = -q / 64 + parts, term, ssum = [], Fr(1), Fr(0) + for k in range(0, 60): + ssum += term + parts.append(ssum) + term = term * g / (k + 1) + lo, hi = min(parts[-1], parts[-2]), max(parts[-1], parts[-2]) + exact = Iv(Iv.frac(lo ** 64).lo, Iv.frac(hi ** 64).hi) + X = Iv.frac(q) + got = (-X).exp() + ok &= got.intersects(exact) and CC.divide(got.width(), got.lo) < Decimal(10) ** (-PREC + 3) + m = 60 + r = math.isqrt(q.numerator * q.denominator * 10 ** (2 * m)) + root = Iv(Iv.frac(Fr(r, q.denominator * 10 ** m)).lo, Iv.frac(Fr(r + 1, q.denominator * 10 ** m)).hi) + ok &= X.sqrt().intersects(root) and CC.divide(X.sqrt().width(), root.lo) < Decimal(10) ** (-PREC + 3) + ok &= (-X).lo == X.hi.copy_negate() and (-X).hi == X.lo.copy_negate() + return ok + + +# ---------------- Taylor arithmetic over intervals +def t_const(c, K): + return [Iv.of(c)] + [Iv(ZERO)] * K + + +def t_var(c, K): + s = t_const(c, K) + s[1] = Iv(ONE) + return s + + +def t_add(u, v): + return [x + y for x, y in zip(u, v)] + + +def t_scale(u, c): + return [x * c for x in u] + + +def t_mul(u, v): + K = len(u) - 1 + out = [] + for k in range(K + 1): + acc = Iv(ZERO) + for j in range(k + 1): + acc = acc + u[j] * v[k - j] + out.append(acc) + return out + + +def t_exp(u): + K = len(u) - 1 + e = [u[0].exp()] + for k in range(1, K + 1): + acc = Iv(ZERO) + for j in range(1, k + 1): + acc = acc + (u[j] * j) * e[k - j] + e.append(acc / k) + return e + + +def t_sqrt(u): + K = len(u) - 1 + s = [u[0].sqrt()] + two_s0 = s[0] * 2 + for k in range(1, K + 1): + acc = u[k] + for j in range(1, k): + acc = acc - s[j] * s[k - j] + s.append(acc / two_s0) + return s + + +def t_ipow(u, n): + out = t_const(1, len(u) - 1) + for _ in range(n): + out = t_mul(out, u) + return out + + +def integrand_series(name, centre, K, k): + """Taylor series at a = centre + t of the raw (unnormalised) integrand of J_hat, T1, T2 or Tb: + gamma^p . poly(a) . exp(-(a^2/4 + beta_0^2/4 + c_0^2/12)) with beta_0 = a^2/(12k), c_0 = a^3/(144k^2).""" + s = Fr(1, 144 * k * k) + a = t_var(centre, K) + a2 = t_mul(a, a) + a4 = t_mul(a2, a2) + a6 = t_mul(a4, a2) + g = t_add(t_const(1, K), t_scale(a2, s)) # gamma^2 = 1 + s a^2 + c_term = Fr(0) if MUT == "cusp-shift" else Fr(1, 248832 * k ** 4) + P = t_add(t_add(t_scale(a2, Fr(-1, 4)), t_scale(a4, -Fr(1, 576 * k * k))), t_scale(a6, -c_term)) + E = t_exp(P) + root = t_sqrt(g) + if name == "J": # gamma^11 = g^5 sqrt(g) (mutant gamma-power: gamma^10 = g^5) + core = t_ipow(g, 5) if MUT == "gamma-power" else t_mul(t_ipow(g, 5), root) + return t_scale(t_mul(core, E), J_SCALE()) + if name == "T1": # gamma^9 (1 + 12 A^2) = g^4 sqrt(g) (1 + 12 s a^2) + w = t_add(t_const(1, K), t_scale(a2, 12 * s)) + return t_scale(t_mul(t_mul(t_mul(t_ipow(g, 4), root), w), E), T1T2_SCALE()) + if name == "T2": # gamma^13 . (-(a^2/24 + a^4/(3456 k^2))) + w = t_add(t_scale(a2, Fr(-1, 24)), t_scale(a4, -Fr(1, 3456 * k * k) * T2_WEIGHT())) + return t_scale(t_mul(t_mul(t_mul(t_ipow(g, 6), root), w), E), T1T2_SCALE()) + if name == "Tb": # |A| gamma^10 = (a/(12k)) g^5 on a >= 0 + w = t_scale(a, Fr(1, 12 * k)) + return t_mul(t_mul(t_ipow(g, TB_POWER()), w), E) + raise ValueError(name) + + +def enclose_half_line(name, k, T, cells, K): + """int_0^T (raw integrand) as an interval, with the per-cell Taylor remainder; K even.""" + h = Fr(T, cells) + if cells % 2 or K % 2: + raise ValueError("cells and K must be even") + total, max_rem, partial = Iv(ZERO), Decimal(0), None + for i in range(cells): + if i == cells // 2: + partial = total # int_0^{T/2}: the truncation-nesting witness + lo, hi = h * i, h * (i + 1) + c = (lo + hi) / 2 + r = Iv.frac(h / 2) + p = integrand_series(name, Iv.frac(c), K, k) + q = integrand_series(name, Iv(Iv.frac(lo).lo, Iv.frac(hi).hi), K, k) + cell, rpow = Iv(ZERO), r + for j in range(K): + if j % 2 == 0: + cell = cell + p[j] * (rpow * Fr(2, j + 1)) + rpow = rpow * r + rem = q[K] * (rpow * Fr(2, K + 1)) + max_rem = max(max_rem, rem.width()) + total = total + cell + rem + return total, max_rem, partial + + +def tail_bound(name, k, T): + """Upper bound of int_T^inf of the raw integrand: gamma^p |poly| <= (1 + s a^2)^7 (1 + a^2)^2 in every case (T >= 1, + a >= T: 1 + 12 s a^2 <= (1 + s a^2)(1 + a^2)... crude but rigorous), times e^{-a^2/4}; the Gaussian moments + int_T^inf a^{2j} e^{-a^2/4} <= T^{-1} 2 4^j j! e^{-T^2/4} sum_{i<=j} (T^2/4)^i/i!.""" + if MUT == "tail-dropped": + return Iv(ZERO) + s = Fr(1, 144 * k * k) + T = Fr(T) + x = T * T / 4 + e = Iv.frac(-x).exp() + # envelope polynomial in a^2: (1 + s a^2)^7 * (1 + a^2)^2 (covers gamma^13, (1+12A^2), |A| <= a and a^2/24 + a^4/(3456k^2) <= (1+a^2)^2) + env = {} + for j in range(8): + for i in range(3): + env[i + j] = env.get(i + j, 0) + comb(7, j) * s ** j * comb(2, i) + tot = Iv(ZERO) + for j, cj in env.items(): + poly = sum(x ** i / factorial(i) for i in range(j + 1)) + tot = tot + e * Iv.frac(Fr(cj) * 2 * 4 ** j * factorial(j) * poly / T) + return Iv(ZERO, tot.hi) + + +def float_reference(name, k): + """Independent floating-point estimate (96-point Gauss-Legendre on [0, 14], doubled) of the raw integral.""" + xs, ws = [], [] + n = 96 + for i in range(1, n + 1): + x = math.cos(math.pi * (i - 0.25) / (n + 0.5)) + for _ in range(100): + p0, p1 = 1.0, x + for m in range(2, n + 1): + p0, p1 = p1, ((2 * m - 1) * x * p1 - (m - 1) * p0) / m + dp = n * (x * p1 - p0) / (x * x - 1) + dx = p1 / dp + x -= dx + if abs(dx) < 1e-16: + break + xs.append(x) + ws.append(2 / ((1 - x * x) * dp * dp)) + kf = float(k) + def raw(a): + g = 1 + (a / (12 * kf)) ** 2 + E = math.exp(-a * a / 4 - a ** 4 / (576 * kf * kf) - a ** 6 / (248832 * kf ** 4)) + if name == "J": + return float(J_SCALE()) * g ** 5.5 * E + if name == "T1": + return float(T1T2_SCALE()) * g ** 4.5 * (1 + 12 * (a / (12 * kf)) ** 2) * E + if name == "T2": + return -float(T1T2_SCALE()) * g ** 6.5 * (a * a / 24 + float(T2_WEIGHT()) * a ** 4 / (3456 * kf * kf)) * E + return (a / (12 * kf)) * g ** TB_POWER() * E + return 2 * sum(w * raw(7 * t + 7) for t, w in zip(xs, ws)) * 7 + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + ap.add_argument("--T", type=int, default=16) + ap.add_argument("--cells", type=int, default=160) + ap.add_argument("--K", type=int, default=12) + args = ap.parse_args() + MUT = args.mutant + if MUT == "context-neg": + setcontext(Context(prec=28, rounding=ROUND_HALF_EVEN, Emin=-9999999, Emax=9999999)) + t0 = time.time() + PI = pi_interval() + LOG2 = log2_interval() + SQRT2, SQRT3 = Iv.frac(2).sqrt(), Iv.frac(3).sqrt() + NORM = 1 / (PI * PI * PI * 192).sqrt() # (2 pi)^(-3/2) 24^(-1/2) + KAPPA = (Iv.frac(Fr(11, 13)).sqrt() * Iv.frac(Fr(11, 13) ** 5)) * Fr(2, 13) # (2/13)(11/13)^(11/2) + D_INNER = Iv.frac(Fr(27066286003, 223205220)) - LOG2 * Fr(79298560, 4782969) + ERF_HALF = erf_interval(Fr(1, 2)) + checks = {} + ok_float, ok_nest, ok_pinned, ok_width, ok_trunc = True, True, True, True, True + out = {"object": "C6-TAIL-CONSTANT-CERTIFIED-20260930-v1", "precision_digits": PREC, "taylor_order": args.K, + "truncation": args.T, "cells": args.cells, "pi": PI.pair(), "log2": LOG2.pair(), "erf_half": ERF_HALF.pair(), + "kappa": KAPPA.pair(), "D_inner": D_INNER.pair(), "raw_integrals": {}, "constants": {}} + raw = {} + for k in KS: + raw[k] = {} + for name in ("J", "T1", "T2", "Tb"): + half, rem, half_T2 = enclose_half_line(name, k, args.T, args.cells, args.K) + sgn = -1 if name == "T2" else 1 # T2's integrand is negative: the tail is subtracted + tail_T, tail_T2 = tail_bound(name, k, args.T), tail_bound(name, k, Fr(args.T, 2)) + val = (half + tail_T * sgn) * 2 + val_T2 = (half_T2 + tail_T2 * sgn) * 2 # enclosure at truncation T/2 (same cells, same K) + coarse_half, _, _ = enclose_half_line(name, k, args.T, max(8, args.cells // 4), max(6, args.K - 4)) + coarse = (coarse_half + tail_T * sgn) * 2 + ok_trunc &= val.lo <= val_T2.hi and val_T2.lo <= val.hi + ref = float_reference(name, k) + tol = abs(Decimal(repr(ref))) * Decimal("1e-11") + ok_float &= val.lo <= Decimal(repr(ref)) + tol and val.hi >= Decimal(repr(ref)) - tol + ok_nest &= coarse.contains(val) + ok_width &= val.width() <= abs(Decimal(repr(ref))) * Decimal("1e-11") + raw[k][name] = val + out["raw_integrals"]["%s|%s" % (name, k)] = {"interval": val.pair(), "width": str(val.width()), + "float_reference_10sig": "%.10g" % ref, "max_cell_remainder_width": str(rem), + "coarse_enclosure": coarse.pair(), "tail_bound_at_T": str(tail_T.hi), + "enclosure_at_half_T": val_T2.pair()} + # exact identities (derived in README section 3): Tb(k) = (12 k^2 + 1)/(36 k^3) and T2 = -T1/12 + ok_tb, ok_t2 = True, True + out["exact_relations"] = {"G0": "exp(-12 k^2 (gamma^6 - 1))", "Tb": "(12 k^2 + 1)/(36 k^3)", "T2": "-T1/12", + "c_prefactor": str(C_PREF), "B_sign_prefactor": str(B_PREF), "per_k": {}} + for k in KS: + tb_exact = Fr(12 * k * k + 1, 36 * k ** 3) + ok_tb &= raw[k]["Tb"].contains(Iv.frac(tb_exact)) + minus_t1_over_12 = raw[k]["T1"] * Fr(-1, 12) + ok_t2 &= raw[k]["T2"].lo <= minus_t1_over_12.hi and minus_t1_over_12.lo <= raw[k]["T2"].hi + out["exact_relations"]["per_k"][str(k)] = {"Tb_exact": str(tb_exact), "Tb_enclosure": raw[k]["Tb"].pair(), + "minus_T1_over_12": minus_t1_over_12.pair(), "T2_enclosure": raw[k]["T2"].pair()} + # universal bounds on c = C_PREF . T1/J_hat: strict containment in (C_LOWER, C_UPPER) at every k + ok_cb = True + for k in KS: + c_iv = raw[k]["T1"] * C_PREF / raw[k]["J"] + ok_cb &= Iv.frac(C_LOWER).hi < c_iv.lo and c_iv.hi < Iv.frac(C_UPPER).lo + out["exact_relations"]["c_bounds"] = {"lower": str(C_LOWER), "upper": str(C_UPPER), + "note": "T1/J_hat = 12 - 11 I_9/I_11 with 0 < I_9 < I_11; both ends are limits (k -> inf, k -> 0)"} + # all-k bounds (README section 3, consequence 3): with s = 4 sqrt3 k sqrt(gamma^6 - 1), J_hat = int F(gamma) e^{-s^2/4} ds + # with 1 <= F = gamma^7 sqrt((gamma^4 + gamma^2 + 1)/3) <= gamma^9 = (1 + s^2/(48 k^2))^{3/2}; likewise I_9 with + # 1 <= F_9 = gamma^5 sqrt(...) <= gamma^7. Hence 2 sqrt(pi) < J_hat(k) <= 2 sqrt(pi)(1 + 1/(16k^2) + 1/(512k^4)), + # 2 sqrt(pi) < I_9(k) <= 2 sqrt(pi)(1 + 7/(144k^2) + 7/(13824k^4)), and the derived bounds on B_sign and c. + ok_kb = True + two_sqrt_pi = PI.sqrt() * 2 + kb = {} + for k in KS: + J_iv = raw[k]["J"] + I9_iv = (J_iv * 12 - raw[k]["T1"]) / 11 + upJ = two_sqrt_pi * (1 + Fr(1, 16 * k * k) + Fr(1, 512 * k ** 4)) + upI9 = two_sqrt_pi * (1 + Fr(7, 144 * k * k) + Fr(7, 13824 * k ** 4)) + tb = Fr(12 * k * k + 1, 36 * k ** 3) + b_lo = Iv.frac(tb) * B_PREF / upJ + b_hi = Iv.frac(tb) * B_PREF / two_sqrt_pi + c_hi = (Iv.frac(12) - two_sqrt_pi * 11 / upJ) * C_PREF + b_iv = Iv.frac(tb) * B_PREF / J_iv + c_iv = raw[k]["T1"] * C_PREF / J_iv + ok_kb &= two_sqrt_pi.hi < J_iv.lo and J_iv.hi < upJ.lo + ok_kb &= two_sqrt_pi.hi < I9_iv.lo and I9_iv.hi < upI9.lo + ok_kb &= b_lo.hi < b_iv.lo and b_iv.hi < b_hi.lo + ok_kb &= c_iv.hi < c_hi.lo + kb[str(k)] = {"J_hat": J_iv.pair(), "J_hat_bounds": [two_sqrt_pi.pair(), upJ.pair()], "I_9": I9_iv.pair(), + "I_9_bounds": [two_sqrt_pi.pair(), upI9.pair()], "B_sign": b_iv.pair(), "B_sign_bounds": [b_lo.pair(), b_hi.pair()], + "c": c_iv.pair(), "c_upper": c_hi.pair()} + out["exact_relations"]["k_dependent_bounds"] = { + "J_hat": "2 sqrt(pi) < J_hat(k) <= 2 sqrt(pi) (1 + 1/(16 k^2) + 1/(512 k^4))", + "I_9": "2 sqrt(pi) < I_9(k) <= 2 sqrt(pi) (1 + 7/(144 k^2) + 7/(13824 k^4))", + "B_sign": "B_PREF (12k^2+1)/(36 k^3) / upJ < B_sign(k) < B_PREF (12k^2+1)/(72 sqrt(pi) k^3)", + "c": "c(k) <= C_PREF (12 - 11 . 2 sqrt(pi)/upJ)", + "asymptotic_series_not_certified": {"J_hat/(2 sqrt pi)": "1 + 1/(18 k^2) + 13/(10368 k^4) - 35/(746496 k^6) + O(k^-8)", + "I_9/(2 sqrt pi)": "1 + 1/(24 k^2) + 1/(10368 k^4) + 0 k^-6 + O(k^-8)", + "c/C_PREF": "1 + 11/(72 k^2) + O(k^-4)"}, + "per_k": kb} + # pinned digits + for key, prefix in PINNED.items(): + if key.startswith("J_hat|"): + v = raw[Fr(key.split("|")[1])]["J"] + elif key == "D": + v = D_INNER + elif key == "log2": + v = LOG2 + elif key == "pi": + v = PI + else: + continue + ok_pinned &= str(v.lo).startswith(prefix) and str(v.hi).startswith(prefix) + # constants per (k, b) + for k in KS: + J, T1, T2, Tb = (raw[k][n] * NORM for n in ("J", "T1", "T2", "Tb")) + for b in BS: + phi_b = Iv.frac(-b * b / 4).exp() / (PI * 2).sqrt() # phi(b/sqrt2) + Phi_b = (ERF_HALF + 1) / 2 if b == 1 else Iv.frac(Fr(1, 2)) # Phi(b/sqrt2), b in {0,1} + m2b = Phi_b * (b * b + 2) + phi_b * SQRT2 * b + pref = phi_b / (SQRT2 * m2b * (36 * k * k)) # p_b(0)/z_0 + if MUT == "prefactor": + pref = pref * Fr(385, 384) + K0 = pref * (108 * k ** 7) + C0 = pref * J * Fr(216 * k ** 7, 11) + Cstar = C0 * I_SHAPE + C2 = K0 * (T1 * U2 + T2 * Fr(2, 13) * BSH) + c_ratio = C2 / Cstar + Bsign = (K0 / Cstar) * Tb * UABS + key = "k=%s,b=%s" % (k, b) + out["constants"][key] = { + "K0": K0.pair(), "C0_per_shape": C0.pair(), "C_star": Cstar.pair(), "C_star_width": str(Cstar.width()), + "G_max": (C0 * (I_SHAPE - D_INNER)).pair(), "G2": (C0 * JOUT).pair(), "B2": (C0 * D_INNER).pair(), + "singleton": (C0 * (I_SHAPE - JOUT - D_INNER)).pair(), + "C2": C2.pair(), "c_C2_over_Cstar": c_ratio.pair(), "dTV_coefficient_kappa_c": (KAPPA * c_ratio).pair(), + "B_sign": Bsign.pair(), "J_cusp": J.pair(), "T1": T1.pair(), "T2": T2.pair(), "Tb": Tb.pair(), + "c_reduced": (raw[k]["T1"] * C_PREF / raw[k]["J"]).pair(), + "B_sign_reduced": (Iv.frac(Fr(12 * k * k + 1, 36 * k ** 3)) * B_PREF / raw[k]["J"]).pair()} + pk = "C_star|%s|%s" % (k, b) + if pk in PINNED: + ok_pinned &= str(Cstar.lo).startswith(PINNED[pk]) and str(Cstar.hi).startswith(PINNED[pk]) + ok_mono = raw[KS[0]]["J"].lo > raw[KS[1]]["J"].hi > raw[KS[2]]["J"].hi and raw[KS[1]]["J"].lo > raw[KS[2]]["J"].hi + ok_pi = ok_pinned and all(v.width() < Decimal("1e-40") for v in (PI, LOG2, ERF_HALF, KAPPA, D_INNER)) + checks = {"FLOAT_INSIDE": bool(ok_float), "NESTING": bool(ok_nest), "WIDTHS": bool(ok_width), "PINNED": bool(ok_pinned), + "MONOTONE_IN_K": bool(ok_mono), "CONSTANTS_RIGOROUS": bool(ok_pi), "TB_EXACT": bool(ok_tb), "T2_IDENTITY": bool(ok_t2), + "TRUNCATION_NESTING": bool(ok_trunc), "C_BOUNDS": bool(ok_cb), "K_BOUNDS": bool(ok_kb), + "LIBRARY_EXACT": bool(library_exact())} + out["checks"] = checks + out["passed"] = all(checks.values()) and len(checks) == 12 + print("elapsed seconds %.1f" % (time.time() - t0), file=sys.stderr) # timing stays out of the pinned output + out["scope"] = ("rigorous enclosures of the one-dimensional cusp integrals and of the assembled constants; the planar " + "reductions and the exact shape integrals are consumed at their records' scopes; not a proof of any " + "theorem; scientific effect NONE") + print(json.dumps(out, indent=2, sort_keys=True)) + return 0 if out["passed"] else 1 + + +if __name__ == "__main__": + sys.exit(main())