Skip to content

Latest commit

 

History

25 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

The Bernstein constant: ten rigorously certified digits

The release's canonical claim, machine-parsable and checked by make headline against RELEASE_CLAIM.json:

BEGIN CERTIFIED ENCLOSURE
lower_endpoint: 0.280169499016595460711186
upper_endpoint: 0.28016949904799999998
rounded_value: 0.2801694990
correctly_rounded_places: 10
END CERTIFIED ENCLOSURE
0.280169499016595460711186  <=  beta  <=  0.28016949904799999998

Ten correctly-rounded decimal places: beta = 0.2801694990. Width 3.140454e-11. Both printed endpoints are rounded outward, so the printed endpoints are themselves proved bounds.

beta = lim_{n->inf} 2n * E_2n(|x|; [-1,1]) is the Bernstein constant: the limiting scaled error of best uniform polynomial approximation to |x| on [-1,1].

This repository is the audit package — the certificate data, the code that produced it, and independent tooling to re-derive and attack it.


Verify it yourself

The headline number is re-derivable with nothing but the Python standard library — no third-party packages, no network:

make stdlib-only          # no third-party imports at all, about a minute

which runs the headline audit, the duplicate-run check and the licence map — all on the standard library alone. Once mpmath and numpy are installed, add the negative suite:

pip install mpmath numpy && make verify-fast

verify-fast is not stdlib-only, despite its position here: one mutation in the negative suite is deliberately invisible to Level 1 and must be caught by Level 2, which needs both packages. The four things it runs:

  • headline — checks the published enclosure and the ten-place digit claim end to end, in exact arithmetic, from the shard data and the two certificates. This is the advertised claim, not a proxy for it.

  • level1b — 36 mutation classes, 37 expected outcomes, each handled by the level responsible. Needs mpmath and numpy: one mutation is deliberately invisible to Level 1 and must be caught by Level 2. Run this before trusting anything else. A checker never shown to fail is not evidence.

  • duplicates — the 600 pole intervals that were accidentally recomputed by a second worker, proven identical. This shows the two runs agreed exactly; it does not by itself prove they were independent processes, since only the recorded commit differs between the two copies.

Then the independent evaluator:

pip install mpmath numpy && make verify     # adds level2, ~1 min

Level 2 evaluates R(t) from the mathematical definition via mpmath digamma, sharing no code with the certifying kernel, and checks |R(t)| against the bound of the region actually containing t — piece-local across all 161 pieces of interval 0, sampling near both sides of every seam.

And with python-flint, the certifier's own strict recombination:

pip install python-flint==0.6.0 && make level3

What each level does and does not establish is tabulated in VERIFY.md. No level re-executes the 436,201,931 branch-and-bound cells; regenerating them is REGENERATION.md.

From the archive, with no network

release_verify.sh is the whole thing end to end: it verifies the archive against its .sha256, refuses any member that is absolute, traversing or a symlink, checks the outer copy of itself byte-for-byte against the archived one, builds a throwaway virtualenv, and runs every gate with a fresh HOME and empty PYTHONPATH.

bash release_verify.sh --wheelhouse wheelhouse bernstein-constant-certificate-1.0.0.tar.gz

With --wheelhouse the dependencies install via pip --no-index, so no step of the run touches the network. The deposit carries the three wheels that directory needs, for CPython 3.9 on macOS arm64:

  • mpmath-1.4.1-py3-none-any.whl
    sha256:dc4f0ea2304480d4a9a48a94c1020571558ade522b44a6912efac63a586e140f
  • numpy-2.0.2-cp39-cp39-macosx_14_0_arm64.whl
    sha256:2b2955fa6f11907cf7a70dab0d0755159bca87755e831e47932367fc8f2f2d0b
  • python_flint-0.6.0-cp39-cp39-macosx_11_0_arm64.whl
    sha256:0d7e366a71bcbba3dfeedf6c5423acad5e9dfb8aa7e508159cac2b0c894a586c

Download them into a directory named wheelhouse and pass it. Each hash can be checked against the file PyPI publishes, so the wheels need not be taken on trust from this deposit. numpy and python-flint are compiled wheels, so on another platform or Python version build the directory once on a connected machine:

pip download -r requirements.txt -d wheelhouse

Without --wheelhouse the run is identical except that the venv build fetches from PyPI.

Gate names

Reviews of this release refer to five gates by name. They exist under those names, as aliases for the level-numbered targets — the alias runs the same checks, it is not a second, weaker path:

checklist name runs establishes does not establish
make headline-audit headline strict parsing, file inventory, hashes, exact rational recombination, endpoint consistency by role, and the ten-place decimal rounding — in exact arithmetic, standard library only it proves no mathematics: it neither proves the lemmas in PROOFS.md nor validates FLINT/Arb. It checks that the claim follows from the data.
make verify-upper level1 level2 level3 revalidates every stored per-interval bound against the strict schema, recomputes the exact rational aggregate from the raw shards, and recomputes the Arb tail bound it does not regenerate the 436,201,931 branch-and-bound cells. The per-interval bounds are read from the shards, not re-derived, so this is recombination-and-tail, not a full recertification. There is also one interval kernel, so a replay is not independent corroboration of it, and it inherits T1, T2 and T4.
make verify-lower level-lower re-derives the lower endpoint on Arb (the rigorous backend) and on mpmath (a nonrigorous numerical cross-check), and requires the live Arb result — not a recorded one — to be at least the published endpoint mpmath agreement is corroboration, not rigour. It cannot be used to overrule an Arb failure.
make negative-tests level1b that the gates can fail: 36 mutation classes, 37 expected outcomes, each rejected by the level responsible a mutation suite bounds what the gates catch; it cannot enumerate what nobody thought to stage.
make release-gate everything above, plus the structural and privacy checks one machine-readable summary, with each line labelled by the kind of evidence it is; nonzero if any required gate fails or is skipped five items are listed MANUAL and are not counted as passing.

What kind of claim each statement is

category what it means here
historical / recorded what the shipped output files say. The shard bounds, cell counts and recorded git_commit ids are of this kind.
rigorous, relative to trusted inputs what the current Arb replay and the exact audit establish, given T1–T3 in TRUSTED_INPUTS.md. Both endpoints, and the ten-place digit claim, are of this kind.
proved here the monotonicity, tail and pole-correction lemmas, in PROOFS.md. make lemmas corroborates them numerically; the proofs are what carry them.
numerical cross-check mpmath evaluation and the Level 2 sampling. Falsification only — passing is evidence, not proof.
unavailable the producer chain of custody, and the exact FLINT/Arb C-library version used in production. Neither is recoverable, and neither is claimed.

Corrections

Substantive post-deposit corrections are released as a new version, with an entry in CHANGELOG.md identifying the superseded version. A published archive is never silently replaced, and a local fix is not a correction until it is deposited.

There is no continuous integration. The gates are run by hand; what the release offers instead is an archive-bound cleanroom transcript of one manually initiated final run. Nothing here should be read as continuous verification.

make full-verify prints the runtime versions first, then runs make release-gate, so a transcript records the environment the gates passed in. make claim-hashes is the one command that writes: it re-records the proof-critical source hashes in RELEASE_CLAIM.json after a deliberate edit. It is not part of any verification path.

Read this before citing

  • NOTE.md — the computational note. Section 5 states plainly what is proved and what is trusted; Section 6 shows why an eleventh place is unreachable with the released witness for a provable reason rather than a budgetary one. It does not claim that no other coefficient vector at the same m could reach it; no optimality of the witness is proved or needed.
  • VERIFY.md — what each verification level establishes, and what it does not.
  • PROOFS.md — proofs of the monotonicity lemmas the branch-and-bound relies on. make lemmas corroborates them numerically.
  • TRUSTED_INPUTS.md — everything relied on but not established here. The list is short: essentially the Varga-Carpenter theorem.
  • PROVENANCE.md — what provenance this release does and does not establish. It establishes internal hash consistency, not a chain of custody.
  • ENVIRONMENT.md — the execution environment, including what is not recorded. The honest page.
  • REGENERATION.md — how to re-derive the shards.
  • LITERATURE.md — the comparison baseline, and what is deliberately not claimed.
  • ACCEPTANCE.md — all 136 acceptance criteria with the gate, document or proof that discharges each. Read this to find the evidence behind any claim without reading the source.
  • CHANGELOG.md — the material repairs made before deposit, including the ones that changed what this release is entitled to claim.

What this is not

Proved digits, not estimated ones. The Varga–Carpenter rigorous enclosure (eq. 1.16) determines five correctly-rounded decimal places, beta = 0.28017. That paper's widely-quoted ~50-digit value (eq. 1.18) is a Richardson extrapolation, described there as "probably accurate to 50 decimal places" — an estimate, not a proved bound, and nothing here rests on it. The ten places certified in this release are proved: every emitted per-interval bound is an exact rational, and the enclosure is 153901× narrower than an outward rendering of the published rigorous pair. That is a comparison against one baseline, not a claim of novelty — see LITERATURE.md.

This is a computational contribution. The underlying inequality beta <= 2 mu_m is classical (Varga and Carpenter 1985, attributing the limiting relation to Bernstein). What is offered is a large-scale rigorous evaluation of it, plus a certificate whose aggregation and digit claim can be re-checked from the raw data. It is not a new theorem in approximation theory and is not presented as one.

No priority claim is made, and none is implied. LITERATURE.md records the Varga–Carpenter enclosure used as the comparison baseline, and nothing else. This release makes no statement about whether later rigorous enclosures exist, about novelty, or about being best known. The author's admission rule requires a subject-matter expert to be contacted before any such statement, and that step is open. If you know of intervening work, please open an issue so the comparison can be corrected.

That open step does not gate this deposit. It gates any claim of novelty, priority, or best-known status — none of which is made here. What is deposited is a scoped computational certificate and its audit trail, and it stands or falls on the checks in VERIFY.md. If a priority claim is ever added, the expert-contact step must close first.

The upper endpoint rests on a single kernel implementation. Eleven parallel workers ran one kernel; that is parallelism, not independent evidence, and a kernel error would be common-mode. The lower endpoint, by contrast, was cross-checked by two independent backends agreeing to 19 decimals. See NOTE.md §5.

Layout

NOTE.md VERIFY.md PROVENANCE.md ENVIRONMENT.md   documentation
PROOFS.md TRUSTED_INPUTS.md
REGENERATION.md LITERATURE.md LICENSES.md
Makefile                                        `make verify`
RELEASE_CLAIM.json                              the released constants, machine-readable;
                                                `make headline` checks the prose against it
mu_kernel_arb.py                                Arb ball-arithmetic kernel
mu_certify_arb.py                               certifier + strict combine
build_upper_certificate.py                      shards -> certificate
verify_enclosure.py                             endpoint/digit verifier (dev-repo bound)
lower_certify_arb.py lower_certify.py           lower endpoint, two backends
mu_certify.py                                   shared mpmath interval F(t) for the
                                                lower backend (helpers only)
audit/                                          schema, aggregation, headline, negative tests
certificates/shards_m64000/                     exactly the 1069-shard partition
witnesses/                                      coefficient witnesses
provenance/                                     duplicate runs, redundant shards
                                                (NO producer git history -- see PROVENANCE.md)

License

Dual-licensed by path — see LICENSES.md for the mapping:

The Zenodo deposition records cc-by-4.0 because Zenodo carries a single record license; that applies to the data and text. Code files retain MIT as stated here and in LICENSES.md.

About

Bernstein's constant to ten rigorously certified digits: beta = 0.2801694990, proved in interval arithmetic (Arb) where the 1985 Varga-Carpenter rigorous enclosure gives five. OEIS A073001. Every number re-derivable from the shipped data in exact arithmetic.

Topics

Resources

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages