Skip to content

Make the repo verify end to end: one entry point, real-data checks, sharper README - #71

Merged
jadenfix merged 9 commits into
mainfrom
sharpen
Oct 18, 2026
Merged

jadenfix merged 9 commits into
mainfrom
sharpen

Conversation

@jadenfix

Copy link
Copy Markdown
Owner

Summary

  • One entry point. uv sync && uv run python -m simtheory verify, or make verify, runs these checks in order:

    1. byte-compiles src/;
    2. validates every claims/*.json manifest: schema, globally unique IDs, evidence files and anchors, file.py:symbol references, nonclaims, and a cited test for every non-open claim;
    3. validates the paper's claim ledger;
    4. recomputes the real-data receipts;
    5. compares the experiment suite with receipts/experiments.txt;
    6. runs pytest and reports, per claim, whether its cited tests passed.

    --quick skips the nine slow exhaustive tests. --online re-downloads the public data. CI runs verify on Python 3.11 to 3.13 from uv.lock.

  • Real data.

    • The Delft 2015 loophole-free Bell test recomputes from the released trials to S = 2.42 +- 0.20, p = 0.039, as published. The point sits right of the S = 2 chord on the canonical CHSH disk.
    • All 256 NIST beacon precommitment links verify, and the composite Bayes factor on 131072 bits never reaches ln 100.
    • Claims ST-F50, ST-F51, ST-F52, ST-T271 and ST-M83 are new. They were renumbered from ST-F32 to F34, ST-T185 and ST-M50, which the merged research PRs already use.
  • Claims. Every non-open claim now cites a passing test, including a direct test for the core result ST-T01. The paper ledger (paper/identifiability-before-anthropic-bayes/claims.json) is checked for unique IDs, assumptions, nonclaims, and the test files its workflow names.

  • Docs. Repairs LaTeX that escape sequences had turned into control characters (\frac became a form feed, \nu a newline) and drops em dashes.

  • README. States the core result plainly. Lists results by type: 262 theorems, 83 model results, 51 finite checks and 1 open problem, across 53 manifests. Adds lanes for the merged Bayesian Boolean, latent-prior and mixture, and active-experiment work.

Verification

uv run python -m simtheory verify (full) on this branch, rebased on main after #47 to #70:

ok    53 manifests, 397 claims (51 finite_check, 83 model_result, 1 open_problem, 262 theorem)
ok    paper/identifiability-before-anthropic-bayes/claims.json: 8 paper claims
ok    Delft 2015: n=245 k=196 S=2.422+-0.204 p=0.0392 disk q=(0.856,-0.094)
ok    NIST beacon: 256 precommitment links verified, 131072 bits, max log BF 1.48 < ln 100
ok    151 lines match receipts/experiments.txt (relative tolerance 1e-9)
ok    587 passed, 0 failed, 0 skipped across 134 files
ok    404 claims have every cited test file passing
verify: all checks passed

A passing check validates code and a bounded receipt. It does not promote a finite check into a theorem, and none of this is evidence for or against simulation.

🤖 Generated with Claude Code

jadenfix and others added 9 commits October 18, 2026 00:01
Nine claims cited no test file, including the core identifiability
result ST-T01 (P_sim = P_base implies BF = 1). Add a direct test for
ST-T01 and for ST-T181/ST-T183 (mixed benchmark gap), cite the existing
test files that exercise ST-T02/T03/T05/T06/T07/M01, and validate every
manifest's evidence paths (quantum-phase-claims.json was never loaded
by any test).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Several formulas had backslash sequences turned into control
characters when written: \frac became a form feed in four docs and
\nu became a newline in the Dobrushin contraction inequality. Restore
them, and replace the remaining em dashes with plain punctuation.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…on bits

Add hash-verified reductions of two public data sets, committed as
small summaries with provenance under data/real/:

- Delft 2015 loophole-free Bell test (4TU doi:10.4121/uuid:6e19e9b2-...):
  the authors' valid-trial filter ported to the standard library keeps
  245 of 4746 attempts and recomputes S = 2.42 +- 0.20, p = 0.039, as
  published; the correlations land at q = (0.856, -0.094) on the
  canonical CHSH disk, right of the S = 2 chord.
- NIST Randomness Beacon chain 2, 257 pulses: all 256 SHA-512
  precommitment links verify, and the Krichevsky-Trofimov composite
  Bayes factor on the 131072 bits never reaches ln 100.

New claims ST-F32..F34 (finite checks), ST-T185 (KL detection-rate
bound for a biased simulator) and ST-M50 (coarsening slows detection),
each with assumptions and nonclaims. python -m simtheory.real_data_fetch
re-downloads and re-reduces both sources.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
python -m simtheory verify (or make verify) byte-compiles src,
validates every claims manifest (schema, unique IDs, evidence files,
anchors, file:symbol references), recomputes the real-data receipts,
compares the experiment suite with receipts/experiments.txt, runs the
tests, and reports per claim whether its cited tests passed. --quick
skips the nine exhaustive tests now marked slow (about ten of the
eleven minutes); --online re-downloads the public data.

Add a dev dependency group and uv.lock, and run verify in CI through
setup-uv on Python 3.11 to 3.13.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Open with the question and the identifiability boundary, give a few
concrete results on the restricted side, tabulate the 266 claims by
type and lane, document verify, and add an explicit scope section and
data credits. The long formula tour moves to docs/result-map.md.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The research PRs merged before this branch already use ST-T185, ST-M50
and ST-F32 to ST-F34 for other results. Renumber the real-data claims to
the next free IDs after them: ST-F50, ST-F51, ST-F52 (Delft statistic,
CHSH-disk placement, NIST beacon Bayes factor), ST-T271 (KL detection rate)
and ST-M83 (coarsening slows detection). The manifest check in verify
already rejects an ID that appears in two manifests.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
paper/<name>/claims.json uses its own schema and IDs (P1-T1, ...), so the
manifest step skipped it. Check each ledger for unique IDs (also against
the repository IDs), assumptions, nonclaims, and the tests/test_paper_* files that the
paper workflow names, and include its claims in the per-claim test report.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The 21 PRs merged before this branch add 131 claims in 18 manifests.
Update the counts (397 claims: 262 theorems, 83 model results, 51 finite
checks, 1 open problem), extend the active-experiment lane, add lanes
for Bayesian Boolean experiments and for latent priors and mixtures,
and point to the paper's own claim ledger and the math audit.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@jadenfix
jadenfix merged commit b74ece2 into main Oct 18, 2026
4 of 7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant