# Proof Assistant Integration Scope
P108 chooses a Lean-first integration path. The reason is pragmatic: Tokitai
already emits Lean-shaped replay skeletons, and Lean can check small standalone
theorem files without requiring a large project scaffold. Coq remains a later
backend candidate; P108 does not attempt a Coq term generator.
## Supported Path
The P108/P123/P124 path has two artifacts:
1. `*.proof-replay.lean`: the existing replay skeleton that preserves theorem
metadata, obligations, evidence, adapter metadata, and statement
fingerprints. This file may still contain `axiom` declarations and is used as
the trace summary source.
2. `*.lean-checkable.lean`: a Lean artifact with no `axiom` declarations. It
still exports one smoke theorem per replay entry using `by trivial`, plus
comments binding the theorem to the Tokitai theorem id, original proof id,
replay rule, status, statement fingerprint, adapter backend, checker
version, proof status, and plan fingerprint. Since P123 it also emits the
selected theorem witness family
`shape_equality_dimension_witness_v1`: each `shape_equality` replay summary
receives an additional Lean theorem named
`<theorem_id>_shape_equality_witness` whose proposition is a concrete
output-shape dimension-count equality discharged by `rfl`.
Since P124 it also emits the selected nonstandard witness family
`padic_precision_cutoff_witness_v1`: each eligible p-adic
`valuation_cutoff` replay summary receives an additional Lean theorem named
`<theorem_id>_padic_precision_cutoff_witness` whose proposition is a concrete
precision/cutoff metadata equality discharged by `rfl`.
The intended checker command is:
```sh
lean <artifact>.lean-checkable.lean
```
If Lean is unavailable in the environment, Tokitai can still record a
deterministic checker transcript for the intended command and bind that
transcript into a checker-output artifact whose digest is bound into a native
admission. This is a scoped offline verification boundary, not a claim that the
local machine ran Lean.
For camera-ready artifact evaluation, optional external Lean execution steps
are documented in `docs/paper/optional_lean_checker.md`. That workflow is
additional evidence and is not required for the default release gate.
## Supported Theorem Classes
P108 checkable smoke artifacts cover theorem classes already replayed by
Tokitai:
- `shape_equality`
- `valuation_cutoff`
- `lowering_semantic_preservation`
- `rewrite_soundness`
The checkable file proves only the Lean-side transport shell for these replayed
entries. Mathematical content remains represented by Tokitai replay predicates,
statement fingerprints, native admission artifacts, and checker result index
bindings.
P123 adds one stronger selected theorem witness family:
- `shape_equality_dimension_witness_v1`: for `shape_equality` replay entries,
the checkable artifact derives a concrete Lean equality from the replayed
`output_shape=[...]` evidence. This is intentionally narrow: it proves a
selected shape witness inside Lean and keeps the broader matrix-shape
inference semantics in Tokitai's replay predicate.
P124 adds one nonstandard-domain selected theorem witness family:
- `padic_precision_cutoff_witness_v1`: for p-adic `valuation_cutoff` replay
entries, the checkable artifact derives a concrete Lean equality from the
replayed `precision=` or `cutoff=` evidence. This supports the SCI-Q2
nonstandard-domain thesis by showing that p-adic planner evidence can be
exported as an external checker witness, while the full non-Archimedean
algebraic soundness argument remains in Tokitai replay predicates and the
formal model.
In short, this is the SCI-Q2 nonstandard-domain thesis witness path.
Broader p-adic algebra and sheaf witness families are planned as
post-submission hardening in `docs/paper/post_submission_witnesses.md`. That
plan preserves the current selected shape and p-adic witness claims and does not make broader witness coverage a P132 submission blocker.
## Trusted Base
The P108 trusted base is:
- Tokitai's proof replay validator.
- Tokitai's Lean smoke artifact generator and parser/validator.
- Tokitai's selected shape equality witness generator and parser/validator.
- Tokitai's selected p-adic precision cutoff witness generator and
parser/validator.
- Tokitai's checker transcript parser/validator and transcript digest binding.
- The SHA-256 digest binding between checker output and native admission.
- The external Lean executable when the checker command is actually run.
## Unsupported Cases
P108 does not claim:
- full Lean proof term generation for all Tokitai obligations;
- Coq or Isabelle output;
- verification of generated Rust, CPU, SIMD, or GPU machine code;
- proof of all p-adic or sheaf mathematics inside Lean;
- full Lean reconstruction of p-adic valuation or sheaf gluing mathematics;
- public-key authenticity of checker outputs.
Those boundaries are deliberate. P108 strengthens the paper claim from
"admission only" to "trace-bound admission plus a minimally checkable Lean
artifact path", while P109 is reserved for signature and trust-model hardening.
## Trace Binding
The native admission `evidence_digest` must equal the digest of the checker
output associated with the checkable Lean artifact. The checker output records:
- artifact filename;
- plan fingerprint;
- checker backend;
- checker version;
- checked theorem count;
- result status;
- checkable artifact digest;
- checker transcript digest.
Trace validation rejects stale checker output when its digest no longer matches
the native admission artifact referenced by the native adapter capability and
checker result index.
## Checker Transcript Binding
P113 adds the `tokitai-proof-assistant-checker-transcript` artifact. The
transcript records the intended `checker_command`, checkable artifact filename,
checkable artifact digest, exit status, stdout digest, stderr digest, and
result status. The accepted Lean-first path uses:
```sh
lean <artifact>.lean-checkable.lean
```
Tokitai validates transcript evidence in four layers:
- smoke checkability: the `.lean-checkable.lean` artifact is no-axiom Lean
syntax intended for a small external check;
- optional local checker invocation: a real Lean executable may produce stdout,
stderr, and exit status for the transcript;
- transcript binding: the checker output must name the same checkable artifact
and include the digest of an accepted transcript;
- native admission binding: the native admission evidence digest must equal the
digest of that checker output.
Trace validation rejects missing checker transcripts, stale checker transcripts
whose artifact digest no longer matches the checker output, and failed checker
transcripts. Failed checker transcripts are transcripts with nonzero exit status
or non-accepted result status. This still does not claim unsupported full
theorem generation for every Tokitai obligation; it strengthens the evidence
boundary between offline proof assistant checks and runtime operator trace
acceptance. Since P123, stale or mismatched selected shape equality witnesses
are detected through the same checkable-artifact digest, checker-output,
native-admission, and checker-index chain.
The required transcript failure cases are: missing checker transcripts, stale
checker transcripts, and failed checker transcripts.
The unsupported boundary remains unsupported full theorem generation for every
Tokitai mathematical obligation.