# Optional External Lean Checker
This document describes an optional external Lean checker workflow for
camera-ready artifact evaluation. It is not required for the default release gate,
and it does not change the P132 no-blocker submission-readiness verdict.
## Scope
The optional Lean workflow provides additional external checker evidence for
the Lean-facing artifacts already generated by Tokitai. It does not replace the
default trace-bound native admission artifact gate.
Default required gate:
- `cargo test`
- `cargo run --quiet --example paper_benchmarks`
- signed audit trace validation from `docs/paper/release_checklist.md`
Optional Lean evidence:
- run `lean <artifact>.lean-checkable.lean` on generated checkable artifacts
when a venue or camera-ready artifact evaluator requests it;
- record stdout, stderr, exit status, Lean version, and artifact digest as
additional evidence;
- keep the generated checker transcript, checker output, native admission, and
checker result index bindings as the repository-grounded validation path.
## P151 Default And Optional Gate Matrix
| `cargo test` | yes | Rust unit, integration, schema, paper-artifact, and trace validation guards | in-repository tests |
| `cargo run --quiet --example paper_benchmarks` | yes | deterministic paper tables and scoped evaluation rows | generated paper CSV/JSON output |
| signed audit trace smoke check | yes | manifest signatures, proof adapter fingerprints, native admissions, checker result indexes, and trace bindings | `matmul.proof-adapters.json`, `tokitai-trace-manifest.json` |
| generated checker transcript binding | yes | external-checker metadata captured by Tokitai even when Lean is not installed | `matmul.checker-transcript.json`, `matmul.checker-output.json` |
| native admission binding | yes | Tokitai-native admission evidence tied to checker output and generated checkable artifacts | `matmul.native-admission.json`, `matmul.checker-result-index.json` |
| optional Lean execution | no | reviewer-requested execution of the generated Lean-facing smoke artifact | `matmul.lean-checkable.lean`, optional Lean evidence/stdout/stderr files |
The default no-Lean validation gate remains unchanged. Optional Lean execution
adds reviewer-facing evidence only; it is not part of the required repository
acceptance path unless the caller explicitly asks for it with
`TOKITAI_REQUIRE_LEAN=1`.
## Environment Expectations
Required for the default release gate:
- Rust toolchain with Cargo.
- `python` for schema validation.
- `rg` for release smoke checks.
Optional for external Lean evidence:
- Lean executable available as `lean`.
- `lean --version` recorded in camera-ready environment capture.
- Access to the generated `*.lean-checkable.lean` artifact from the signed audit
trace directory.
## Generate A Checkable Artifact
Run the signed audit trace example with a temporary output directory:
```bash
tmpdir=$(mktemp -d)
TOKITAI_AUDIT_TRACE_DIR="$tmpdir" \
TOKITAI_AUDIT_TRACE_KEY_ID="test key" \
TOKITAI_AUDIT_TRACE_SECRET="trace-secret" \
cargo run --quiet --example audit_traces
```
Expected Lean-facing files include:
- `$tmpdir/matmul.lean-checkable.lean`
- `$tmpdir/matmul.checker-transcript.json`
- `$tmpdir/matmul.checker-output.json`
- `$tmpdir/matmul.native-admission.json`
- `$tmpdir/matmul.checker-result-index.json`
- `$tmpdir/tokitai-trace-manifest.json`
## Optional Lean Command
If Lean is available, run:
```bash
lean "$tmpdir/matmul.lean-checkable.lean"
```
Record:
```bash
lean --version
sha256sum "$tmpdir/matmul.lean-checkable.lean"
```
If the platform does not provide `sha256sum`, use the platform's equivalent
SHA-256 command and record the command in artifact notes.
## P151 Optional Execution Wrapper
The repository includes a reviewer-facing helper:
```bash
scripts/optional_lean_check.sh
```
With no arguments, the helper generates a signed audit trace in
`target/tokitai-optional-lean` or in `TOKITAI_AUDIT_TRACE_DIR` when that
environment variable is set, then looks for `matmul.lean-checkable.lean`. The
default `audit_traces` example currently emits the `.proof-replay.lean`
skeleton and trace manifest path; if no generated `.lean-checkable.lean` file is
present, the helper writes skipped evidence with
`reason=checkable_artifact_not_generated_by_default_audit_trace` rather than
claiming an external Lean run occurred.
When a checkable artifact is present, or when a reviewer supplies one from a
native checker fixture or paper artifact run, check it explicitly:
```bash
scripts/optional_lean_check.sh "$tmpdir/matmul.lean-checkable.lean" "$tmpdir"
```
The script records:
- `optional-lean-evidence.txt` status evidence, including `status=skipped` and
`reason=lean_not_found` when Lean is unavailable;
- `reason=checkable_artifact_not_generated_by_default_audit_trace` when the
no-argument convenience path only produced the default trace skeleton and no
`.lean-checkable.lean` artifact;
- `audit-traces.stdout` and `audit-traces.stderr` for the no-argument trace
generation convenience path;
- `lean --version` output when Lean is available;
- artifact SHA-256 through `sha256sum` or the platform fallback `shasum -a 256`;
- stdout, stderr, and exit status for `lean "$artifact"`;
- `default_gate=unchanged_no_lean`, documenting that the default cargo and
paper-benchmark gates are unchanged.
By default, missing Lean or a failed Lean run is non-blocking and the helper
exits successfully after writing evidence. To make optional Lean execution
strict for a camera-ready artifact build, run:
```bash
TOKITAI_REQUIRE_LEAN=1 scripts/optional_lean_check.sh "$tmpdir/matmul.lean-checkable.lean" "$tmpdir"
```
When `TOKITAI_REQUIRE_LEAN=1`, missing Lean or a nonzero Lean exit status
returns a nonzero script status. This strict mode is a reviewer-packaging
option, not the default Tokitai validation gate.
## P263 Selected-Theorem Profile
P263 defines a mandatory proof-assistant evidence profile that can be enabled
for a selected theorem subset with `TOKITAI_REQUIRE_LEAN=1`. The selected subset
is intentionally narrow:
- `docs/theorems/padic_valuation_skip.lean`: valuation-skip, dot-product, and
matrix-output p-adic valuation theorems.
- `docs/theorems/finite_sheaf_gluing.lean`: finite-sheaf gluing and
incompatible-overlap obstruction theorems.
The theorem checker scripts write
`evidence_profile=selected-theorem-strict-capable`, `selected_theorems=...`,
the Lean status, transcript paths when Lean runs, timeout policy, and whether
strict mode was required. The theory release gate checks that this profile is
present and that strict commands are listed. This does not claim full
proof-assistant formalization of Tokitai or verification of the Rust runtime.
## Expected Result
The optional Lean command should accept the generated checkable artifact. The
artifact is intentionally narrow:
- it contains no `axiom` declarations;
- it includes selected witness family metadata;
- it includes `shape_equality_dimension_witness_v1`;
- it includes `padic_precision_cutoff_witness_v1` when p-adic precision cutoff
witness evidence is present;
- smoke theorems and selected witnesses are discharged by simple Lean terms
such as `trivial` or `rfl`.
## Binding Back To Tokitai
After running the optional checker, keep the standard Tokitai validation checks:
```bash
test -f "$tmpdir/matmul.proof-adapters.json"
rg -Fq '"capability_fingerprint":"sha256:' "$tmpdir/matmul.proof-adapters.json"
rg -Fq '"adapter_capability_fingerprint":"sha256:' "$tmpdir/tokitai-trace-manifest.json"
```
The external Lean run is additional evidence. The repository's trace acceptance
still depends on checkable artifact digests, checker transcript metadata,
checker output digests, native admission evidence, adapter capability
fingerprints, checker result indexes, and trace manifest bindings.
## Non-Goals
This workflow does not claim:
- full Lean proof term generation for all Tokitai obligations;
- full Coq or Isabelle theorem generation;
- full Lean reconstruction of p-adic valuation or sheaf gluing mathematics;
- verification of Rust, CPU, SIMD, or GPU machine code;
- replacement of Tokitai's proof replay predicates or formal model;
- that Lean execution is required before SCI-Q2 submission.
## Relationship To Other Release Documents
- `docs/paper/proof_assistant_scope.md` defines the supported proof-assistant
boundary.
- `docs/paper/post_submission_packaging.md` treats Lean as optional
camera-ready evidence.
- `docs/paper/release_checklist.md` keeps the default release gate no-Lean.
- `docs/paper/final_submission_readiness.md` keeps the P132 no repository-level
submission blockers verdict.