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