Lean guide — Proof Path Theory 1.8.0
Fresh record
The release builds and replays 18 production modules, auditing 283 explicit named declarations, including 169 named theorems. The 13 earlier modules are unchanged. Five new modules implement the current continuation. Counts include helpers and concrete examples and do not assert historical novelty.
| Module | New mathematical role |
|---|---|
| Trace | Executable strict/causal replay; soundness, extensivity, composition; accepted complete closure and protected verdicts. |
| TraceCompleteness | Causal weakening, finite premise-trace assembly, derivation-to-trace existence, complete forbidden-node witnesses. |
| TraceWire | Exact JSON AST codec, general round trips, injectivity, validity checks, decoded-answer soundness, bounded derived addresses. |
| TraceExamples | Checked good and bad records, cycles, empty inputs, duplicate rule rows, malformed types and changed observations. |
| TraceFixtures | Six generated actual exchange pairs with acceptance and semantic theorems. |
The independent IO consumer formal/CheckTraceJson.lean is not one of the 18
proved production modules. It uses the standard JSON parser/printer and reads
canonical NDJSON. Its 83,994-case execution has zero mismatches against the
independent finite model oracle. This is byte-level conformance evidence, not
a universal proof of parsing or operating-system behavior.
Trust inventory
The compiler hash and nine dependency revisions are checked. Source scans
reject proof placeholders and extra trusted production axioms. All recorded
transitive axioms are among propext, Classical.choice, and Quot.sound.
Ten deliberately invalid proof controls must fail for specified proof diagnostics.
An eleventh uses an explicit false axiom: Lean accepts its consequence relative
to that axiom, and the separate axiom policy rejects that dependency.
The record is evidence/formal_1.8.0/verification.json. Per-declaration types can
be inspected in the sources; locations, hashes, axiom sets and related claim
groups are indexed by formal/CONCORDANCE.json. The new groups are PPT-042–047.
python scripts/verify_lean.py --runtime /path/to/portable-kit
This is Lean's own-kernel replay against pinned cached imports, not a second
kernel implementation or a fresh rebuild of every Mathlib dependency. Original
evidence is retained with its original versions. The older total-output decoder
remains distinct from ProofPath.Recovery.Sufficient on attained outputs.
The checker proof does not certify arbitrary Python execution, byte parsers, source adapters, or the entire monograph. The semantic validity of labels still requires a sound declared interpretation. Entropy and social models retain their separate written/conditional scopes.