Edition README
Proof Path Theory
README.md
1 # Proof Path Theory — monograph edition 1.8.0
2
3 **Komorebi P. · Operation Komorebi**
4
5 Certificates, compression, discovery fields, and mathematical memory.
6
7 ## The publication
8
9 The **76-page** monograph is `docs/Proof_Path_Theory.pdf`, with editable LaTeX
10 in the adjacent `.tex` file. It retains the five-part monograph design and adds
11 one mathematical illustration: **25 numbered vector figures**, one cover motif,
12 and **six worked visual studies**. The eight-page sampler is extracted from this
13 edition, not copied from a predecessor.
14
15 The 41 prior result groups and all 149 prior mathematical environments remain.
16 Six new groups and fourteen new statement/proof environments establish a precise
17 checker and exchange contract. Publication **1.8.0** and Python distribution
18 **1.6.0** have distinct versions. The original named-field schemas and provenance
19 encoding are unchanged; the new positional trace format has its own version tag.
20
21 ## What is newly proved
22
23 An executable Lean replay checker refines the existing `Field` and seeded
24 closure, not a new semantics defined to agree with program output. Accepted
25 complete traces certify the **least** seeded model. Both derivability and a
26 final saturation check are necessary. A forbidden-node witness is a causal trace,
27 and one exists exactly when the fixed protected problem is infeasible.
28
29 The typed problem and certificate codecs have proved left inverses and hence
30 are injective at Lean's `Json` syntax-tree boundary. Acceptance of decoded
31 records gives the same protected closure/feasibility theorem. Unknown addresses,
32 boolean-as-integer inputs, invented nodes, incomplete closures, and changed
33 observations have explicit negative tests.
34
35 ## Reproducible exchange
36
37 ```bash
38 python scripts/check_manifest.py
39 python -m pip install -e ".[release]" --no-build-isolation
40 proof-path wire-export examples/and_dag.json --negative B --output-prefix trial
41 proof-path wire-check trial.problem.json trial.certificate.json
42 ```
43
44 The request, proposed result, and source address book are separate files.
45 An accepted negative result is an obstruction for that request. A rejected
46 certificate is not an infeasibility verdict. See `docs/TRACE_EXCHANGE.md` for
47 syntax, resource limits, trust boundaries, and the Lean consumer.
48
49 ## Current evidence
50
51 - **18** production Lean modules freshly built and replayed by Lean's own kernel.
52 - **283** explicit named-declaration axiom audits, including **169** named theorems.
53 - **233** source-package tests and the same suite against an installed wheel.
54 - **83,994** serialized cases matched by the independent model oracle, Python
55 checker, and actual Lean JSON consumer, with zero verdict mismatches.
56 - Existing exhaustive protected, semantic-cover, linear, recovery, retention,
57 and covariance checks are rerun separately and retain their declared domains.
58
59 The mathematical theorem counts, result groups, concrete examples, and test
60 counts are different inventories. None is a count of novel discoveries.
61
62 Current records:
63
64 ```text
65 evidence/formal_1.8.0/verification.json
66 data/release_verification.json
67 data/publication_verification_1.8.0.json
68 data/trace_exchange_1.8.0.json
69 data/recovery_extension_checks_1.8.0.json
70 formal/CONCORDANCE.json
71 PROGRESS_LEDGER_v1.8.0.md
72 ```
73
74 The 13 preceding production Lean modules are unchanged. Five new modules are
75 `Trace`, `TraceCompleteness`, `TraceWire`, `TraceExamples`, and `TraceFixtures`.
76 The IO adapter `CheckTraceJson.lean` is executed but not counted as a proved IO
77 implementation. The pinned compiler and nine dependency revisions are checked;
78 Mathlib's cached imports are not freshly rebuilt as a whole.
79
80 ## Rebuild and verify
81
82 Use a fresh working copy. Rebuilding changes evidence hashes; check the supplied
83 manifest before running rebuild commands, not after.
84
85 ```bash
86 python -m pytest -o addopts='' -q
87 python scripts/deep_validation.py
88 python scripts/verify_bridge.py
89 python scripts/check_recovery_extension.py
90 python scripts/check_trace_exchange.py
91 python scripts/design_figures.py
92 python scripts/verify_lean.py --runtime /path/to/portable-kit
93 python scripts/verify_release.py --runtime /path/to/portable-kit
94 ```
95
96 The full release verifier obtains a new formal run, rebuilds the manuscript,
97 builds a wheel and source distribution, tests the installed wheel separately,
98 and checks publication/source correspondence. The publication-only verifier
99 checks recorded evidence and source identity; it does not invoke Lean.
100
101 Figures need an installed Lato font. Font files and the large offline Lean kit
102 are not distributed in this package. pdfLaTeX, NewTX, Source Sans Pro, TikZ,
103 and the other declared preamble packages are needed for the manuscript.
104 Installation may access a package index unless dependencies are supplied locally.
105 The finite computation and verification commands use no model API.
106
107 ## Boundaries and rights
108
109 The JSON AST codec and the Lean Boolean checker are proved. The text parser,
110 printer, IO, Python producer/checker, and source-to-index adapter are not thereby
111 universally verified. Concrete cross-language agreement is tested evidence.
112 The original named proof fields remain acyclic; cyclic checker fixtures use the
113 separate lower-level indexed domain. Semantic interpretation still requires
114 sound leaves/rules and true positive observations. Social models remain
115 conditional and are not empirically established by these tests.
116
117 The existing license notice is unchanged. No license was chosen on the author's
118 behalf. Hosted CI, native Windows execution, and all supported Python versions
119 were not run here. Current Linux/Python and pinned Lean runs are recorded.