From 30de5e327a61228479238679896ef4701024e67f Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Wed, 30 Sep 2026 13:28:15 +0000 Subject: [PATCH 1/4] Certified enclosures of the planar microscopic radius-tail constants reviews/c6_tail_constant_certified_20260930/: rigorous interval enclosures (decimal interval arithmetic, order-12 Taylor models with interval remainders, exact Gaussian tail bound, series-bracketed pi, log 2, erf(1/2); stdlib only) of the cusp integrals J_hat, T_1, T_2, T_b and of C_*, G_max, G_2, B_2, singleton, C_2, c, kappa c, B_sign for k in {1/2, 1, 2}, b in {0, 1}. Every value of Math-#178 RESULTS.json lies within 9e-16 relative of its enclosure. Two exact identities recorded and enforced as interval checks: T_b(k) = (12k^2 + 1)/(36k^3) and T_2 = -T_1/12, so c = (66451/11128) T_1/J_hat and B_sign = (4587821/876544) T_b/J_hat. Nine rules, eight mutants, workflow verifying the manifest, three main pins by blob, both interpreter modes and the mutants. Scientific effect NONE; no register, catalog or STATUS change. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../workflows/c6-tail-constant-certified.yml | 78 ++ .../README.md | 186 +++++ .../RESULTS.json | 740 ++++++++++++++++++ .../SOURCE_FILES.json | 77 ++ .../certify_tail_constants.py | 467 +++++++++++ 5 files changed, 1548 insertions(+) create mode 100644 .github/workflows/c6-tail-constant-certified.yml create mode 100644 reviews/c6_tail_constant_certified_20260930/README.md create mode 100644 reviews/c6_tail_constant_certified_20260930/RESULTS.json create mode 100644 reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json create mode 100644 reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py diff --git a/.github/workflows/c6-tail-constant-certified.yml b/.github/workflows/c6-tail-constant-certified.yml new file mode 100644 index 000000000..5c3c7e414 --- /dev/null +++ b/.github/workflows/c6-tail-constant-certified.yml @@ -0,0 +1,78 @@ +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' + 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'] + 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']) == 9 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..70be75608 --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/README.md @@ -0,0 +1,186 @@ +# 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)` with the geometric tail; `erf(1/2)` from its Maclaurin series with + the alternating tail; `sqrt2`, `sqrt3` by interval `sqrt`. +- **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 nine 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; `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` is bracketed below `1e-40` and the pins hold; `TB_EXACT` and + `T2_IDENTITY` the two exact identities of section 3 hold as interval statements. +- **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`). + +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 eight 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.** Writing `I_p(k) = int gamma^p G_0 da`, the whole table depends on two transcendental numbers per `k`, +`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. Asymptotic remark +(not certified, not used): expanding `G_0` and `gamma^11` in `s = 1/(144 k^2)` gives `J_hat(k) = 2 sqrt(pi) (1 + 1/(18 k^2) + O(k^-4))`; +at `k = 2` this reads `3.5941` against the certified `3.59442`, at `k = 1` `3.7418` against `3.74614`. + +## 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 eight mutants under each mode in parallel, clean tree). + + 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 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..fce80c5b8 --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/RESULTS.json @@ -0,0 +1,740 @@ +{ + "D_inner": [ + "109.769950345687984746091911144321148127026343196", + "109.769950345687984746091911144468320649237084123" + ], + "cells": 160, + "checks": { + "CONSTANTS_RIGOROUS": true, + "FLOAT_INSIDE": 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.820060477332820453427583913757742807836694959954", + "0.820060477332820453437420585882569706109227699900" + ], + "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.8011242872557355415190836848898317416363896025", + "51.8011242872557355421404411205174589525479987189" + ], + "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.8943235718723715978812749117863959879075169191", + "22.8943235718723715981558936267431165609227345840" + ] + }, + "k=1,b=1": { + "B2": [ + "0.234790665991551752188175905327808133991381084643", + "0.234790665991551752190992232736782031621510120175" + ], + "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.8311262482411020552353177613993700599846282503", + "14.8311262482411020554132179653017762879171310455" + ], + "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.55485007197146985824484444907536413129400745835", + "6.55485007197146985832347024895312639441792852052" + ] + }, + "k=1/2,b=0": { + "B2": [ + "0.0300730372048412614003608893447228558810155553698", + "0.0300730372048412616976612059478997210060144513237" + ], + "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.89963689386656051709247043218083081775347969605", + "1.89963689386656053587217153555362574118760662435" + ], + "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.839574474794698040695586593492479764422397467595", + "0.839574474794698048995571575660979404718397249642" + ] + }, + "k=1/2,b=1": { + "B2": [ + "0.00861018013778482542350275775963928843929315969046", + "0.00861018013778482550862250351520689245063072016368" + ], + "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.543883071775006473267498057380618488159298349695", + "0.543883071775006478644294831594223050423180651400" + ], + "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.240377698395714561976535149446821329980774234087", + "0.240377698395714564352895254034959623207940005972" + ] + }, + "k=2,b=0": { + "B2": [ + "25.1791005913738603498149535940914194756408718846", + "25.1791005913738603498257873480172744774072910339" + ], + "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.49942684376068348187376715429568468016179718", + "1590.49942684376068348255810769673344881462095957" + ], + "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.946297402991702841491792912479397187305562854", + "702.946297402991702841794248004496603600418243445" + ] + }, + "k=2,b=1": { + "B2": [ + "7.20900221425698565807093095780426650692772983230", + "7.20900221425698565807403275867109177337125814956" + ], + "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.374243741623525694500461385422621211626402597", + "455.374243741623525694696394217409074781693169574" + ], + "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.259826421997460922918308354969530367941134443", + "201.259826421997460923004903959135484061843565631" + ] + } + }, + "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_prefactor": "66451/11128", + "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.693147180559945309417232121449394191788735906002", + "0.693147180559945309417232121458271044172761357528" + ], + "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": "3.7461417283657297", + "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": "4.396080052560472", + "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": "3.5944178057317844", + "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": "4.331219538486052", + "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": "7.201715670125964", + "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": "3.7326066139490246", + "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": "-0.3609349615405044", + "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": "-0.6001429725104974", + "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": "-0.3110505511624188", + "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": "0.36111111111111066", + "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": "0.8888888888888884", + "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": "0.17013888888888878", + "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..893225985 --- /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": 15018, + "sha256": "72323efb8a1d854c93c83faddef6e0a65816e8335b2553b0092addcc5eb9d927", + "git_blob": "70be756087457b9d99558c3ee5765748cb97a203" + }, + { + "path": "RESULTS.json", + "bytes": 28363, + "sha256": "945a28504a75008352e7aecc89f824a8d90211d812b3bceb8a78d88234e4e465", + "git_blob": "fce80c5b80eca1d786726bbba13228670f6c91c4" + }, + { + "path": "certify_tail_constants.py", + "bytes": 20894, + "sha256": "aa084608795af0804d41bd0601b5259a2c0242d3d80e8e494a11faff43e39fd0", + "git_blob": "9a5d01f4446d86cd92126a80e52abf7c2d559c41" + } + ] +} 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..9a5d01f44 --- /dev/null +++ b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py @@ -0,0 +1,467 @@ +"""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. + +Nine rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, +TB_EXACT, T2_IDENTITY; README section 2) and eight mutants must exit 1. 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. +""" +import argparse +import json +import math +import sys +import time +from decimal import Decimal, Context, ROUND_FLOOR, ROUND_CEILING, ROUND_HALF_EVEN +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") +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 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) +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) +# 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): + return Iv(-a.hi, -a.lo) + + 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, 2 * ulp(lo))), CC.add(hi, 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, 2 * ulp(lo))), CC.add(hi, 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 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 = 90 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() + + +# ---------------- 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_mul(core, E) + 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_mul(t_mul(t_mul(t_ipow(g, 4), root), w), E) + 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_mul(t_mul(t_mul(t_ipow(g, 6), root), w), E) + 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 g ** 5.5 * E + if name == "T1": + return g ** 4.5 * (1 + 12 * (a / (12 * kf)) ** 2) * E + if name == "T2": + return -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 + 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": repr(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()} + # 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 = PI.width() < Decimal("1e-40") and ok_pinned + 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)} + out["checks"] = checks + out["passed"] = all(checks.values()) and len(checks) == 9 + 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()) From 65ac384e1b1cba434ee25db6a2c40cc7d0cbd907 Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Wed, 30 Sep 2026 13:57:37 +0000 Subject: [PATCH 2/4] Certified tail constants v1.1: universal bounds on c, Codex findings reviews/c6_tail_constant_certified_20260930/: rule C_BOUNDS (with mutant t1t2-scale) checks the consequence of T_2 = -T_1/12 that 66451/11128 < c(k) = C_2/C_* < 199353/2782 for every k > 0 (T_1/J_hat = 12 - 11 I_9/I_11 with 0 < I_9 < I_11; both ends sharp as limits), which sharpens the corollary bound c > 4587/856 of the merged radial-rate record. Codex review 5366990451: the floating-point control enters the pinned output only to 10 significant digits, so RESULTS.json is byte-identical across CPython versions; log 2 to N = 160 terms and CONSTANTS_RIGOROUS now requires pi, log 2, erf(1/2), kappa and D bracketed below 1e-40; the workflow triggers on all three pinned sources. Ten rules, nine mutants, both interpreter modes byte-identical; enclosures of the integrals and constants unchanged. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../workflows/c6-tail-constant-certified.yml | 6 +- .../README.md | 47 ++++++-- .../RESULTS.json | 110 +++++++++--------- .../SOURCE_FILES.json | 18 +-- .../certify_tail_constants.py | 46 +++++--- 5 files changed, 138 insertions(+), 89 deletions(-) diff --git a/.github/workflows/c6-tail-constant-certified.yml b/.github/workflows/c6-tail-constant-certified.yml index 5c3c7e414..27b3d944f 100644 --- a/.github/workflows/c6-tail-constant-certified.yml +++ b/.github/workflows/c6-tail-constant-certified.yml @@ -6,6 +6,8 @@ name: C6 tail constants certified enclosure - '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: @@ -56,7 +58,7 @@ jobs: 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'] + mutants = ['gamma-power', 'cusp-shift', 'prefactor', 'pi-truncated', 'log2-truncated', 'tail-dropped', 'tb-power', 't2-weight', 't1t2-scale'] def mutant_rc(args): flags, m = args return m, flags, subprocess.run([sys.executable, *flags, script, '--mutant', m], @@ -67,7 +69,7 @@ jobs: 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']) == 9 and all(doc['checks'].values())): + if not (doc['passed'] and len(doc['checks']) == 10 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]): diff --git a/reviews/c6_tail_constant_certified_20260930/README.md b/reviews/c6_tail_constant_certified_20260930/README.md index 70be75608..eabd2886e 100644 --- a/reviews/c6_tail_constant_certified_20260930/README.md +++ b/reviews/c6_tail_constant_certified_20260930/README.md @@ -44,8 +44,9 @@ Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than 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)` with the geometric tail; `erf(1/2)` from its Maclaurin series with - the alternating tail; `sqrt2`, `sqrt3` by interval `sqrt`. + 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 @@ -59,22 +60,27 @@ Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than (`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 nine must hold; `passed` is `false` and the exit code `1` otherwise).** +- **Rules (all ten 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; `NESTING` a coarser enclosure (a quarter of the cells, order `K - 4`) contains the fine one; + 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` is bracketed below `1e-40` and the pins hold; `TB_EXACT` and - `T2_IDENTITY` the two exact identities of section 3 hold as interval statements. + 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`. - **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`). + `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`). 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 eight mutants +script in both interpreter modes, compares the output byte for byte with `RESULTS.json`, and runs the nine 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) @@ -108,9 +114,23 @@ of `-T_1/12` intersect at every `k`, at widths of `1e-16` to `1e-21`), and 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.** Writing `I_p(k) = int gamma^p G_0 da`, the whole table depends on two transcendental numbers per `k`, -`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. Asymptotic remark +**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`. Asymptotic remark (not certified, not used): expanding `G_0` and `gamma^11` in `s = 1/(144 k^2)` gives `J_hat(k) = 2 sqrt(pi) (1 + 1/(18 k^2) + O(k^-4))`; at `k = 2` this reads `3.5941` against the certified `3.59442`, at `k = 1` `3.7418` against `3.74614`. @@ -180,7 +200,10 @@ quadrature, different arithmetic) and does not consume its numbers except in thi 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 eight mutants under each mode in parallel, clean tree). +the nine 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 diff --git a/reviews/c6_tail_constant_certified_20260930/RESULTS.json b/reviews/c6_tail_constant_certified_20260930/RESULTS.json index fce80c5b8..317eb466c 100644 --- a/reviews/c6_tail_constant_certified_20260930/RESULTS.json +++ b/reviews/c6_tail_constant_certified_20260930/RESULTS.json @@ -1,11 +1,12 @@ { "D_inner": [ - "109.769950345687984746091911144321148127026343196", - "109.769950345687984746091911144468320649237084123" + "109.769950345687984746091911144322714480157052373", + "109.769950345687984746091911144322714480157052375" ], "cells": 160, "checks": { "CONSTANTS_RIGOROUS": true, + "C_BOUNDS": true, "FLOAT_INSIDE": true, "MONOTONE_IN_K": true, "NESTING": true, @@ -18,8 +19,8 @@ "constants": { "k=1,b=0": { "B2": [ - "0.820060477332820453427583913757742807836694959954", - "0.820060477332820453437420585882569706109227699900" + "0.820060477332820453427583913757754509621126819120", + "0.820060477332820453437420585881481923303985092503" ], "B_sign": [ "0.504532783579960197454103040229546843535934710651", @@ -47,8 +48,8 @@ "28.9068007153833639439845474937743423916252641351" ], "G_max": [ - "51.8011242872557355415190836848898317416363896025", - "51.8011242872557355421404411205174589525479987189" + "51.8011242872557355415190836848909195244416322099", + "51.8011242872557355421404411205174472507635668597" ], "J_cusp": [ "0.0485521851560528317659531596156492181850366540727", @@ -83,14 +84,14 @@ "0.423807239840966445793630399574743081596795358924" ], "singleton": [ - "22.8943235718723715978812749117863959879075169191", - "22.8943235718723715981558936267431165609227345840" + "22.8943235718723715978812749117874837707127595265", + "22.8943235718723715981558936267431048591383027248" ] }, "k=1,b=1": { "B2": [ - "0.234790665991551752188175905327808133991381084643", - "0.234790665991551752190992232736782031621510120175" + "0.234790665991551752188175905327811484317163131482", + "0.234790665991551752190992232736470589653074155705" ], "B_sign": [ "0.504532783579960197454103040229546843535934710619", @@ -118,8 +119,8 @@ "8.27627617626963219708974771634864989349920252497" ], "G_max": [ - "14.8311262482411020552353177613993700599846282503", - "14.8311262482411020554132179653017762879171310455" + "14.8311262482411020552353177613996815019530642148", + "14.8311262482411020554132179653017729375913489987" ], "J_cusp": [ "0.0485521851560528317659531596156492181850366540727", @@ -154,14 +155,14 @@ "0.423807239840966445793630399574743081596795358949" ], "singleton": [ - "6.55485007197146985824484444907536413129400745835", - "6.55485007197146985832347024895312639441792852052" + "6.55485007197146985824484444907567557326244342282", + "6.55485007197146985832347024895312304409214647367" ] }, "k=1/2,b=0": { "B2": [ - "0.0300730372048412614003608893447228558810155553698", - "0.0300730372048412616976612059478997210060144513237" + "0.0300730372048412614003608893447232850057061231747", + "0.0300730372048412616976612059478598301276255260783" ], "B_sign": [ "1.05831421352984302111038636415859780503065954361", @@ -189,8 +190,8 @@ "1.06006241907186248687659995989264633646920937471" ], "G_max": [ - "1.89963689386656051709247043218083081775347969605", - "1.89963689386656053587217153555362574118760662435" + "1.89963689386656051709247043218087070863186862129", + "1.89963689386656053587217153555362531206291605654" ], "J_cusp": [ "0.0569757655073718298483949476989128256181921250274", @@ -225,14 +226,14 @@ "0.600499647330249788480531471131129824099919074838" ], "singleton": [ - "0.839574474794698040695586593492479764422397467595", - "0.839574474794698048995571575660979404718397249642" + "0.839574474794698040695586593492519655300786392840", + "0.839574474794698048995571575660978975593706681836" ] }, "k=1/2,b=1": { "B2": [ - "0.00861018013778482542350275775963928843929315969046", - "0.00861018013778482550862250351520689245063072016368" + "0.00861018013778482542350275775963941130153890469838", + "0.00861018013778482550862250351519547133455110378639" ], "B_sign": [ "1.05831421352984302111038636415859780503065954357", @@ -260,8 +261,8 @@ "0.303505373379291914291399577559263427215240645429" ], "G_max": [ - "0.543883071775006473267498057380618488159298349695", - "0.543883071775006478644294831594223050423180651400" + "0.543883071775006473267498057380629909275377966073", + "0.543883071775006478644294831594222927560934906392" ], "J_cusp": [ "0.0569757655073718298483949476989128256181921250274", @@ -296,14 +297,14 @@ "0.600499647330249788480531471131129824099919074857" ], "singleton": [ - "0.240377698395714561976535149446821329980774234087", - "0.240377698395714564352895254034959623207940005972" + "0.240377698395714561976535149446832751096853850464", + "0.240377698395714564352895254034959500345694260964" ] }, "k=2,b=0": { "B2": [ - "25.1791005913738603498149535940914194756408718846", - "25.1791005913738603498257873480172744774072910339" + "25.1791005913738603498149535940917787667120214764", + "25.1791005913738603498257873479838752423120304875" ], "B_sign": [ "0.247746643295296011750602312428032120528047229641", @@ -331,8 +332,8 @@ "887.553129440768980640763859692236845214202716128" ], "G_max": [ - "1590.49942684376068348187376715429568468016179718", - "1590.49942684376068348255810769673344881462095957" + "1590.49942684376068348187376715432908391525705772", + "1590.49942684376068348255810769673308952354980998" ], "J_cusp": [ "0.0465857544872538436674809505145367473878549108631", @@ -367,14 +368,14 @@ "0.380650182414239118964379319482752607829251307347" ], "singleton": [ - "702.946297402991702841491792912479397187305562854", - "702.946297402991702841794248004496603600418243445" + "702.946297402991702841491792912512796422400823401", + "702.946297402991702841794248004496244309347093852" ] }, "k=2,b=1": { "B2": [ - "7.20900221425698565807093095780426650692772983230", - "7.20900221425698565807403275867109177337125814956" + "7.20900221425698565807093095780436937518222052396", + "7.20900221425698565807403275866152927296015488846" ], "B_sign": [ "0.247746643295296011750602312428032120528047229636", @@ -402,8 +403,8 @@ "254.114417319626064771691490258273590719849603944" ], "G_max": [ - "455.374243741623525694500461385422621211626402597", - "455.374243741623525694696394217409074781693169574" + "455.374243741623525694500461385432183712037505858", + "455.374243741623525694696394217408971913438678882" ], "J_cusp": [ "0.0465857544872538436674809505145367473878549108631", @@ -438,8 +439,8 @@ "0.380650182414239118964379319482752607829251307357" ], "singleton": [ - "201.259826421997460922918308354969530367941134443", - "201.259826421997460923004903959135484061843565631" + "201.259826421997460922918308354979092868352237704", + "201.259826421997460923004903959135381193589074940" ] } }, @@ -452,6 +453,11 @@ "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", "per_k": { "1": { @@ -506,8 +512,8 @@ "0.0613843941821676280477188642920775402962871118476" ], "log2": [ - "0.693147180559945309417232121449394191788735906002", - "0.693147180559945309417232121458271044172761357528" + "0.693147180559945309417232121458176568075500134360", + "0.693147180559945309417232121458176568075500134361" ], "object": "C6-TAIL-CONSTANT-CERTIFIED-20260930-v1", "passed": true, @@ -526,7 +532,7 @@ "3.74614172830673384075315554254170651708102059456", "3.75027725260702018231699243816832075691318839936" ], - "float_reference": "3.7461417283657297", + "float_reference_10sig": "3.746141728", "interval": [ "3.74614172836573455033513841998214633256472187646", "3.74614172836573455038007360333691238118122447828" @@ -544,7 +550,7 @@ "4.39608005256047628984657685915077717227612500764", "4.88338636508862619334623971076851614454862582206" ], - "float_reference": "4.396080052560472", + "float_reference_10sig": "4.396080053", "interval": [ "4.39608005256047628984657690235788762705235688108", "4.39608005256047633330597152674136876691298772436" @@ -562,7 +568,7 @@ "3.59441779293996319066325662486836917181403587930", "3.59500855337833238063115278410442542179757241854" ], - "float_reference": "3.5944178057317844", + "float_reference_10sig": "3.594417806", "interval": [ "3.59441780573178757508336100029782500857967171872", "3.59441780573178757508490756220742747016140332740" @@ -580,7 +586,7 @@ "4.33121953822329624601780335004655369058166078410", "4.33535506252358258769153318608467375891175381196" ], - "float_reference": "4.331219538486052", + "float_reference_10sig": "4.331219538", "interval": [ "4.33121953848605580811164102859146318962900744216", "4.33121953848605580826648661035356675144025755148" @@ -598,7 +604,7 @@ "7.20171567012596993212913812382198594393315933852", "7.68902198265412002545526287697702991717020433876" ], - "float_reference": "7.201715670125964", + "float_reference_10sig": "7.20171567", "interval": [ "7.20171567012596993212913847208820502602365892024", "7.20171567012597016541499499800915536791448947388" @@ -616,7 +622,7 @@ "3.73260658646099722786050074527686975310092239614", "3.73319734689936641782975153808620982806073412484" ], - "float_reference": "3.7326066139490246", + "float_reference_10sig": "3.732606614", "interval": [ "3.73260661394902762562459046604684882364008944774", "3.73260661394902762562749304884051439081302966826" @@ -634,7 +640,7 @@ "-0.365070485496240399550346221915389782079150339902", "-0.360934961195954057887438364740434401523191902062" ], - "float_reference": "-0.3609349615405044", + "float_reference_10sig": "-0.3609349615", "interval": [ "-0.360934961540504650756162793462443870156345266422", "-0.360934961540504650612122570874516774947553040520" @@ -652,7 +658,7 @@ "-1.08744928503864746141330002138713933112874928731", "-0.600142972510497413163932805935240337465407677130" ], - "float_reference": "-0.6001429725104974", + "float_reference_10sig": "-0.6001429725", "interval": [ "-0.600142972510497601373032699862262101370897738080", "-0.600142972510497413163933711644056007251692398162" @@ -670,7 +676,7 @@ "-0.311641266924490796780306586134670095950311265966", "-0.311050506486121606810088168415933590451284075044" ], - "float_reference": "-0.3110505511624188", + "float_reference_10sig": "-0.3110505512", "interval": [ "-0.311050551162418968804123602699942006633239403652", "-0.311050551162418968800250720715110201707467156868" @@ -688,7 +694,7 @@ "0.361111111078053558425933873185099410625468084994", "0.365246635378339899968849781659484400185135045946" ], - "float_reference": "0.36111111111111066", + "float_reference_10sig": "0.3611111111", "interval": [ "0.361111111111111111100981979010184105434315929778", "0.361111111111111111124994512192976729559760014656" @@ -706,7 +712,7 @@ "0.888888888888888876361424943743882319520634723480", "1.37619520141703876844745916313348311268771294836" ], - "float_reference": "0.8888888888888884", + "float_reference_10sig": "0.8888888889", "interval": [ "0.888888888888888876361424978359559634087704282170", "0.888888888888888908407190970514898421028490976696" @@ -724,7 +730,7 @@ "0.170138884755738839737704086392721482615205220531", "0.170729645194108029704522357987856065959794837027" ], - "float_reference": "0.17013888888888878", + "float_reference_10sig": "0.1701388889", "interval": [ "0.170138888888888888888673361143316460152471457000", "0.170138888888888888889141518067306514606320109713" diff --git a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json index 893225985..2d9d0c16e 100644 --- a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json +++ b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json @@ -57,21 +57,21 @@ "files": [ { "path": "README.md", - "bytes": 15018, - "sha256": "72323efb8a1d854c93c83faddef6e0a65816e8335b2553b0092addcc5eb9d927", - "git_blob": "70be756087457b9d99558c3ee5765748cb97a203" + "bytes": 17221, + "sha256": "272141e0cdd5f8911f9c6dd0c7002a56f50b054024654b423022839a93a7b89d", + "git_blob": "eabd2886e33e70a14c3a10999c14a714bb968bd0" }, { "path": "RESULTS.json", - "bytes": 28363, - "sha256": "945a28504a75008352e7aecc89f824a8d90211d812b3bceb8a78d88234e4e465", - "git_blob": "fce80c5b80eca1d786726bbba13228670f6c91c4" + "bytes": 28569, + "sha256": "51cae9baab6197f1367f165f1af06c426306f25f8f9b06c0f817bb8cd68076bc", + "git_blob": "317eb466c3fb32a8790fb5d1e4d87d6d0e274c09" }, { "path": "certify_tail_constants.py", - "bytes": 20894, - "sha256": "aa084608795af0804d41bd0601b5259a2c0242d3d80e8e494a11faff43e39fd0", - "git_blob": "9a5d01f4446d86cd92126a80e52abf7c2d559c41" + "bytes": 22386, + "sha256": "abc20d8c9ddf2c8542a94f6a641af12726c9fbc3e30e98d796625efe28a06b1b", + "git_blob": "b90b4310fa2e59939860f44816e8701d4096fd3c" } ] } diff --git a/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py index 9a5d01f44..b90b4310f 100644 --- a/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py +++ b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py @@ -22,10 +22,12 @@ The reductions are consumed at those records' stated scopes; this script certifies the arithmetic of the constants, not the theorems. Scientific effect: NONE. -Nine rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, -TB_EXACT, T2_IDENTITY; README section 2) and eight mutants must exit 1. TB_EXACT and T2_IDENTITY are the exact +Ten rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, +TB_EXACT, T2_IDENTITY, C_BOUNDS; README section 2) and nine 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 = (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). """ import argparse import json @@ -36,7 +38,8 @@ 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") +MUTANTS = ("gamma-power", "cusp-shift", "prefactor", "pi-truncated", "log2-truncated", "tail-dropped", "tb-power", "t2-weight", + "t1t2-scale") MUT = None @@ -45,6 +48,12 @@ def T2_WEIGHT(): 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 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 @@ -59,6 +68,8 @@ def TB_POWER(): # 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", @@ -166,8 +177,8 @@ def atan_inv(n, terms): def log2_interval(): - # log 2 = sum_{n>=1} 1/(n 2^n); tail after N terms <= 1/((N+1) 2^N) - N = 90 if MUT != "log2-truncated" else 8 + # 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)) @@ -264,10 +275,10 @@ def integrand_series(name, centre, K, k): return t_mul(core, E) 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_mul(t_mul(t_mul(t_ipow(g, 4), root), w), E) + 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_mul(t_mul(t_mul(t_ipow(g, 6), root), w), E) + 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) @@ -345,9 +356,9 @@ def raw(a): if name == "J": return g ** 5.5 * E if name == "T1": - return g ** 4.5 * (1 + 12 * (a / (12 * kf)) ** 2) * E + return float(T1T2_SCALE()) * g ** 4.5 * (1 + 12 * (a / (12 * kf)) ** 2) * E if name == "T2": - return -g ** 6.5 * (a * a / 24 + float(T2_WEIGHT()) * a ** 4 / (3456 * kf * kf)) * E + 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 @@ -393,7 +404,7 @@ def main(): 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": repr(ref), "max_cell_remainder_width": str(rem), + "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 @@ -407,6 +418,13 @@ def main(): 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)"} # pinned digits for key, prefix in PINNED.items(): if key.startswith("J_hat|"): @@ -449,12 +467,12 @@ def main(): 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 = PI.width() < Decimal("1e-40") and ok_pinned + 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)} + "TRUNCATION_NESTING": bool(ok_trunc), "C_BOUNDS": bool(ok_cb)} out["checks"] = checks - out["passed"] = all(checks.values()) and len(checks) == 9 + out["passed"] = all(checks.values()) and len(checks) == 10 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 " From ca4215501106b72baeeb4b89d7a5f35fd9eee970 Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Wed, 30 Sep 2026 15:51:15 +0000 Subject: [PATCH 3/4] Certified tail constants v1.2: explicit bounds for every k reviews/c6_tail_constant_certified_20260930/: with s = 4 sqrt3 k sqrt(gamma^6 - 1) the cusp integral is 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/(48k^2))^{3/2}, hence 2 sqrt(pi) < J_hat(k) <= 2 sqrt(pi)(1 + 1/(16k^2) + 1/(512k^4)) and 2 sqrt(pi) < I_9(k) <= 2 sqrt(pi)(1 + 7/(144k^2) + 7/(13824k^4)) for every k > 0, with the derived two-sided bound on B_sign(k) = O(1/k), the upper bound on c(k) with an explicit rate, and a lower bound on C_*. Rule K_BOUNDS checks the certified values against these intervals; mutant j-scale. README section 3 Consequence 3 with the derivation and the exact asymptotic series 1 + 1/(18k^2) + 13/(10368k^4) - 35/(746496k^6) (not certified). Eleven rules, ten mutants, both interpreter modes byte-identical; enclosures unchanged. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../workflows/c6-tail-constant-certified.yml | 4 +- .../README.md | 47 ++++- .../RESULTS.json | 170 ++++++++++++++++++ .../SOURCE_FILES.json | 18 +- .../certify_tail_constants.py | 57 +++++- 5 files changed, 269 insertions(+), 27 deletions(-) diff --git a/.github/workflows/c6-tail-constant-certified.yml b/.github/workflows/c6-tail-constant-certified.yml index 27b3d944f..f40f944a7 100644 --- a/.github/workflows/c6-tail-constant-certified.yml +++ b/.github/workflows/c6-tail-constant-certified.yml @@ -58,7 +58,7 @@ jobs: 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'] + mutants = ['gamma-power', 'cusp-shift', 'prefactor', 'pi-truncated', 'log2-truncated', 'tail-dropped', 'tb-power', 't2-weight', 't1t2-scale', 'j-scale'] def mutant_rc(args): flags, m = args return m, flags, subprocess.run([sys.executable, *flags, script, '--mutant', m], @@ -69,7 +69,7 @@ jobs: 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']) == 10 and all(doc['checks'].values())): + if not (doc['passed'] and len(doc['checks']) == 11 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]): diff --git a/reviews/c6_tail_constant_certified_20260930/README.md b/reviews/c6_tail_constant_certified_20260930/README.md index eabd2886e..aaae1320b 100644 --- a/reviews/c6_tail_constant_certified_20260930/README.md +++ b/reviews/c6_tail_constant_certified_20260930/README.md @@ -60,7 +60,7 @@ Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than (`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 ten must hold; `passed` is `false` and the exit code `1` otherwise).** +- **Rules (all eleven 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, @@ -71,16 +71,19 @@ Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than 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`. + 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. - **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`). + 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`). 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 nine mutants +script in both interpreter modes, compares the output byte for byte with `RESULTS.json`, and runs the ten 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) @@ -130,9 +133,37 @@ at the scope of [Q] (13) (aligned planar cusp density of the parent kernel). Bot (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`. Asymptotic remark -(not certified, not used): expanding `G_0` and `gamma^11` in `s = 1/(144 k^2)` gives `J_hat(k) = 2 sqrt(pi) (1 + 1/(18 k^2) + O(k^-4))`; -at `k = 2` this reads `3.5941` against the certified `3.59442`, at `k = 1` `3.7418` against `3.74614`. +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 @@ -200,7 +231,7 @@ quadrature, different arithmetic) and does not consume its numbers except in thi 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 nine mutants under each mode in parallel, clean tree; triggered by changes to the packet, the workflow or any of the +the ten 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). diff --git a/reviews/c6_tail_constant_certified_20260930/RESULTS.json b/reviews/c6_tail_constant_certified_20260930/RESULTS.json index 317eb466c..31ffa7000 100644 --- a/reviews/c6_tail_constant_certified_20260930/RESULTS.json +++ b/reviews/c6_tail_constant_certified_20260930/RESULTS.json @@ -8,6 +8,7 @@ "CONSTANTS_RIGOROUS": true, "C_BOUNDS": true, "FLOAT_INSIDE": true, + "K_BOUNDS": true, "MONOTONE_IN_K": true, "NESTING": true, "PINNED": true, @@ -459,6 +460,175 @@ "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": [ diff --git a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json index 2d9d0c16e..10b1b772d 100644 --- a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json +++ b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json @@ -57,21 +57,21 @@ "files": [ { "path": "README.md", - "bytes": 17221, - "sha256": "272141e0cdd5f8911f9c6dd0c7002a56f50b054024654b423022839a93a7b89d", - "git_blob": "eabd2886e33e70a14c3a10999c14a714bb968bd0" + "bytes": 19710, + "sha256": "5ada0c59fe97db40c38927f1f779544079d376c54dc04c911a2d0dd2f4aec617", + "git_blob": "aaae1320b8c4cb9af50dc185de778861c8ba363d" }, { "path": "RESULTS.json", - "bytes": 28569, - "sha256": "51cae9baab6197f1367f165f1af06c426306f25f8f9b06c0f817bb8cd68076bc", - "git_blob": "317eb466c3fb32a8790fb5d1e4d87d6d0e274c09" + "bytes": 35045, + "sha256": "5c35273a6a14da272d54e8e8e6bd23d39a9999f93e1ed2b205a48802f9bd6e3f", + "git_blob": "31ffa700002e4d92823f9547d9b52d81354155cd" }, { "path": "certify_tail_constants.py", - "bytes": 22386, - "sha256": "abc20d8c9ddf2c8542a94f6a641af12726c9fbc3e30e98d796625efe28a06b1b", - "git_blob": "b90b4310fa2e59939860f44816e8701d4096fd3c" + "bytes": 25264, + "sha256": "5f4979fc477adec90ec6ba2c8d0595efede7a08663aa1d251c33771a6fcae34c", + "git_blob": "1c2bece482bf3e0f1a5a966cc64c03d2fd8999c6" } ] } diff --git a/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py index b90b4310f..1c2bece48 100644 --- a/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py +++ b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py @@ -22,12 +22,13 @@ The reductions are consumed at those records' stated scopes; this script certifies the arithmetic of the constants, not the theorems. Scientific effect: NONE. -Ten rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, -TB_EXACT, T2_IDENTITY, C_BOUNDS; README section 2) and nine mutants must exit 1. The floating-point control enters the +Eleven rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, +TB_EXACT, T2_IDENTITY, C_BOUNDS, K_BOUNDS; README section 2) and ten 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). +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 @@ -39,7 +40,7 @@ from math import comb, factorial MUTANTS = ("gamma-power", "cusp-shift", "prefactor", "pi-truncated", "log2-truncated", "tail-dropped", "tb-power", "t2-weight", - "t1t2-scale") + "t1t2-scale", "j-scale") MUT = None @@ -54,6 +55,12 @@ def T1T2_SCALE(): 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 @@ -272,7 +279,7 @@ def integrand_series(name, centre, K, k): 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_mul(core, E) + 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()) @@ -354,7 +361,7 @@ 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 g ** 5.5 * E + 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": @@ -425,6 +432,40 @@ def main(): 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|"): @@ -470,9 +511,9 @@ def main(): 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)} + "TRUNCATION_NESTING": bool(ok_trunc), "C_BOUNDS": bool(ok_cb), "K_BOUNDS": bool(ok_kb)} out["checks"] = checks - out["passed"] = all(checks.values()) and len(checks) == 10 + out["passed"] = all(checks.values()) and len(checks) == 11 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 " From c9789d9c3496640199a2b0a7fb740dfc2282fba6 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Wed, 30 Sep 2026 17:30:12 +0000 Subject: [PATCH 4/4] Certified tail constants v1.3: exact interval negation, rule LIBRARY_EXACT, mutant context-neg (values unchanged) Rigor repair of the interval class in reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py: endpoints were negated with the Decimal unary minus, which rounds its operand to the thread's current context (default precision 28) rather than to the 48-digit contexts every other step names. In this script the operation never meets an endpoint longer than 28 digits and the repaired script reproduces all 167 intervals of v1.2 byte for byte; the defect was found in the sibling packet frontiers/c8_window_coefficient_planar_20260930, where exp(-x) at a 60-digit x went wrong beyond the 28th digit. Changes: 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; new rule LIBRARY_EXACT compares the decimal module's exp and sqrt, and the interval negation, 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); new mutant context-neg reinstates the v1.2 negation and the 28-digit current context and is caught only by that rule. Twelve rules, eleven mutants; RESULTS.json differs from v1.2 only by the new rule's entry; README section 2, section 7 and new section 8 (revisions); workflow expects twelve checks and runs the eleven mutants. Scientific effect NONE; no register surface touched. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../workflows/c6-tail-constant-certified.yml | 4 +- .../README.md | 32 +++++++++-- .../RESULTS.json | 1 + .../SOURCE_FILES.json | 18 +++--- .../certify_tail_constants.py | 56 ++++++++++++++++--- 5 files changed, 85 insertions(+), 26 deletions(-) diff --git a/.github/workflows/c6-tail-constant-certified.yml b/.github/workflows/c6-tail-constant-certified.yml index f40f944a7..3ac90f6b0 100644 --- a/.github/workflows/c6-tail-constant-certified.yml +++ b/.github/workflows/c6-tail-constant-certified.yml @@ -58,7 +58,7 @@ jobs: 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'] + 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], @@ -69,7 +69,7 @@ jobs: 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']) == 11 and all(doc['checks'].values())): + 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]): diff --git a/reviews/c6_tail_constant_certified_20260930/README.md b/reviews/c6_tail_constant_certified_20260930/README.md index aaae1320b..5f96b3d36 100644 --- a/reviews/c6_tail_constant_certified_20260930/README.md +++ b/reviews/c6_tail_constant_certified_20260930/README.md @@ -60,7 +60,7 @@ Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than (`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 eleven must hold; `passed` is `false` and the exit code `1` otherwise).** +- **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, @@ -73,17 +73,23 @@ Also certified, as a by-product: `pi`, `log 2`, `erf(1/2)` and `D` to more than `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. + (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`). + 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 ten mutants +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) @@ -231,10 +237,24 @@ quadrature, different arithmetic) and does not consume its numbers except in thi 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 ten 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 +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 index 31ffa7000..2735dc391 100644 --- a/reviews/c6_tail_constant_certified_20260930/RESULTS.json +++ b/reviews/c6_tail_constant_certified_20260930/RESULTS.json @@ -9,6 +9,7 @@ "C_BOUNDS": true, "FLOAT_INSIDE": true, "K_BOUNDS": true, + "LIBRARY_EXACT": true, "MONOTONE_IN_K": true, "NESTING": true, "PINNED": true, diff --git a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json index 10b1b772d..725fc903e 100644 --- a/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json +++ b/reviews/c6_tail_constant_certified_20260930/SOURCE_FILES.json @@ -57,21 +57,21 @@ "files": [ { "path": "README.md", - "bytes": 19710, - "sha256": "5ada0c59fe97db40c38927f1f779544079d376c54dc04c911a2d0dd2f4aec617", - "git_blob": "aaae1320b8c4cb9af50dc185de778861c8ba363d" + "bytes": 21599, + "sha256": "f207c320cbe3a676f8a683d5c26a0b74cf66d74d7fec708bf7a6b3517e70b799", + "git_blob": "5f96b3d36defbcd7e32fbb4e9b1d0053aa55d047" }, { "path": "RESULTS.json", - "bytes": 35045, - "sha256": "5c35273a6a14da272d54e8e8e6bd23d39a9999f93e1ed2b205a48802f9bd6e3f", - "git_blob": "31ffa700002e4d92823f9547d9b52d81354155cd" + "bytes": 35072, + "sha256": "c595d223a0f6f9df297443469024094225d0da8f388e1d7c2ed9dbbc59f3e8ec", + "git_blob": "2735dc391818bb431ea7fa3842dde44d1748ea04" }, { "path": "certify_tail_constants.py", - "bytes": 25264, - "sha256": "5f4979fc477adec90ec6ba2c8d0595efede7a08663aa1d251c33771a6fcae34c", - "git_blob": "1c2bece482bf3e0f1a5a966cc64c03d2fd8999c6" + "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 index 1c2bece48..aa590e2b2 100644 --- a/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py +++ b/reviews/c6_tail_constant_certified_20260930/certify_tail_constants.py @@ -22,8 +22,8 @@ The reductions are consumed at those records' stated scopes; this script certifies the arithmetic of the constants, not the theorems. Scientific effect: NONE. -Eleven rules must hold (FLOAT_INSIDE, NESTING, TRUNCATION_NESTING, WIDTHS, PINNED, MONOTONE_IN_K, CONSTANTS_RIGOROUS, -TB_EXACT, T2_IDENTITY, C_BOUNDS, K_BOUNDS; README section 2) and ten mutants must exit 1. The floating-point control enters the +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 @@ -35,12 +35,12 @@ import math import sys import time -from decimal import Decimal, Context, ROUND_FLOOR, ROUND_CEILING, ROUND_HALF_EVEN +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") + "t1t2-scale", "j-scale", "context-neg") MUT = None @@ -68,6 +68,11 @@ def TB_POWER(): 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)) @@ -118,7 +123,9 @@ def __add__(a, b): __radd__ = __add__ def __neg__(a): - return Iv(-a.hi, -a.lo) + 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) @@ -145,13 +152,13 @@ def __rtruediv__(a, b): def exp(a): lo, hi = CE.exp(a.lo), CE.exp(a.hi) - return Iv(max(ZERO, CF.subtract(lo, 2 * ulp(lo))), CC.add(hi, 2 * ulp(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, 2 * ulp(lo))), CC.add(hi, 2 * ulp(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) @@ -160,6 +167,9 @@ 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) @@ -204,6 +214,31 @@ def erf_interval(x): 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 @@ -379,6 +414,8 @@ def main(): 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() @@ -511,9 +548,10 @@ def main(): 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)} + "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) == 11 + 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 "