judgeauto

Reusable local automation for Lean/Lake judge protocols.

This repo centralizes the judge scripts that were previously split between the entropic-time verification tree and the Kuchar/problem-of-time statement repo. It is intentionally small: it does not contain problem solutions, build caches, or generated verdict artifacts.

Contents

• judgeauto/: Python package with reusable protocol and judge logic.
• profiles/kuchar.json: Kuchar problem-of-time profile.
• examples/kuchar/physlib-minimal-protocol.json: protocol JSON matching the Physlib minimal Kuchar candidate harness.
• legacy/entropic-time/: copied shell automations from the entropic-time repo for reference and migration.
• scripts/judgeauto: convenience wrapper for python3 -m judgeauto.cli.

Paper-grounded Kuchar profile

The Kuchar profile is grounded in Karel V. Kuchar, "Time and Interpretations of Quantum Gravity", International Journal of Modern Physics D, Vol. 20, Suppl. 1 (2011), pp. 3-86, DOI 10.1142/S0218271811019347. The detailed judge boundary and paper anchors are documented in docs/kuchar-judge-protocol.md.

The judge checks exact Lean declarations. It does not certify that the physical assumptions behind those declarations are the final correct assumptions for the problem of time.

For the current local Kuchar problem root, theorem formulas are documented as fenced LaTeX in docs/kuchar-theorem-equations.md inside the problem repo.

Kuchar/Physlib local judge

Run the same check that was verified in leandogo-probleme-time:

cd /Users/macbookpro/lab/tau/tau-information-dynamics/judgeauto
python3 -m judgeauto.cli judge   --problem-root /Users/macbookpro/lab/tau/tau-information-dynamics/leandogo-probleme-time   --profile profiles/kuchar.json   --build-candidate   --output verification/kuchar-last-verdict.json   /Users/macbookpro/lab/tau/tau-information-dynamics/leandogo-probleme-time/candidates/physlib-minimal-kuchar

Expected result for the current local candidate:

VERDICT: SOLUTION ACCEPTED
completed targets: obstruction, uniqueness of Physlib-backed obstruction predicate
sorry: 0  axioms: 0  unsafe: 0

The candidate remains outside this repo. judgeauto only verifies it.

Protocol schema

A candidate repo provides a protocol file, such as .kuchar-protocol.json:

{
  "module": "Candidate.KucharSolution",
  "checks": [
    {
      "name": "Physlib-backed obstruction-aware Kuchar target",
      "target": "obstruction",
      "declaration": "Candidate.KucharSolution.kucharWithPhyslibObstructions",
      "obstruction": "Candidate.KucharSolution.HasPhyslibKucharObstruction"
    }
  ]
}

The current Kuchar example also checks a uniqueness proof for the Physlib-backed obstruction predicate.

The selected profile maps target names to exact Lean types. The Kuchar profile maps obstruction to:

Problems.KucharTime.KucharConstraintProblemWithObstructions <obstruction>

Make targets

The common workflows are also available through make:

make help
make smoke
make protocol-check
make judge
make verify

Defaults point at the current local Kuchar/Physlib candidate. Override paths from the command line when judging another package:

make judge \
  PROBLEM_ROOT=/path/to/problem-repo \
  CANDIDATE=/path/to/candidate-repo \
  PROFILE=profiles/kuchar.json

Useful variables:

• PYTHON: Python executable, default python3.
• PROFILE: judge profile JSON, default profiles/kuchar.json.
• PROBLEM_ROOT: problem statement Lake package root.
• CANDIDATE: candidate repo or path.
• OUTPUT: verdict JSON path.
• LEDGER: JSONL ledger path.
• WORK_DIR: temporary judge work directory.

Commands

Describe a profile:

python3 -m judgeauto.cli describe --profile profiles/kuchar.json

Run only the exact Lean protocol check:

python3 -m judgeauto.cli protocol-check   --problem-root /path/to/problem-repo   --profile profiles/kuchar.json   --build-candidate   /path/to/candidate-repo   --json

Run full local judge:

python3 -m judgeauto.cli judge   --problem-root /path/to/problem-repo   --profile profiles/kuchar.json   --build-candidate   /path/to/candidate-repo

The full judge performs:

• Lake build of the problem statement package.
• Optional Lake build of the candidate package.
• Exact Lean #check interface verification.
• Static rejection of bare sorry, unsafe, and axioms by default.
• Candidate source hashing.
• JSONL ledger append.

Notes

• The judge checks that stated Lean declarations have exact expected types. It does not decide whether the physical assumptions behind a declaration are the right assumptions.
• For path dependencies, the judge reads lake-manifest.json and adds local dependency .lake/build/lib/lean directories to LEAN_PATH.
• Generated files under .judgeauto-work/, ledger/, and verification/ are ignored by Git.