25 Reference implementation
On this page · Permalink · Source line 2189
The repository implements the finite theory as the Python package proof_path_theory. The public modules are organized by mathematical responsibility.
| Module | Responsibility |
|---|---|
model.py | Typed nodes, justifications, evidence records, acyclicity, ancestry, and finite derivability. |
certificate.py | Certificate validation, unique AND-DAG cores, exact minimum certificate search, and certificate cost. |
compression.py | Task sufficiency, recoverability preorder, loss reports, compression debt, representation utilities, and Pareto fronts. |
bridges.py | Reachability, domination-based criticality, exact retention, greedy retention, and finite submodularity checks. |
review.py | Equicorrelated covariance, effective reviewer count, generalized least squares, and shared-bias mean squared error. |
audit.py | Audit queue simulation, rate regimes, and explicit priority scores. |
refinement.py | Goal-relative refinement decisions, optimal depth, and stopping rules. |
versioning.py | Affected descendants, append-only checks, ledger snapshots, and provenance digests. |
ambient.py | Finite declared view fibers, restriction checks, and arrow-cover gluing. |
realization.py | Exact binary elimination, protected fibers, obstruction witnesses, and observation gain. |
views.py | Local field models, whole-support gluing, declared countermodels, and intersection diagrams. |
extension.py | Least models preserving true and false observations, with replayable forbidden-node derivations. |
semantic_cover.py | Entailment certificates for redundant supports, countermodels to universal gluing, and checked semantic gluing. |
recovery.py | Factorization on explicit archive families, collision witnesses, joint task schemes, and decoder composition. |
trace_codec.py | Versioned indexed exchange, strict and causal trace replay, and an independent result checker. |
io.py | Stable JSON import and export for proof fields and certificates. |
cli.py | Command-line validation, core extraction, minimum certificate search, and certificate audit. |
25.1 Command-line interface
On this page · Permalink · Source line 2221
The main commands are:
proof-path validate examples/and_dag.json
proof-path core examples/and_dag.json --output core.json
proof-path minimum examples/alternative_proofs.json --output minimum.json
proof-path audit examples/and_dag.json core.json25.2 JSON contract
On this page · Permalink · Source line 2234
A proof field file contains:
a schema version and metadata.
required premises and targets.
typed nodes with value and cost vectors.
typed evidence records with scope and certification flags.
justifications with premise sets, conclusions, rules, evidence references, and certification flags.
The named proof-field schema is intentionally plain. It can be produced by a proof assistant adapter, a research notebook, a theorem ledger, or a hand-written example. The positional trace-exchange format in Section 9.13 is a separate, versioned contract. Neither an imported certification flag nor a successful schema check establishes semantic validity.
25.3 Tests and build discipline
On this page · Permalink · Source line 2247
The regression suite covers graph validation, derivability, certificate extraction, alternative proofs, schema boundaries, and input validation. It also exercises loss vectors, task sufficiency, bridge coverage, retention, review covariance, audit queues, refinement, version propagation, JSON round trips, and the command line. The dated verification record gives the executed count for each edition.
A separate deterministic cross-check compares the exact certificate solver with brute-force enumeration over eighteen cost profiles, tests the greedy cardinality guarantee on one hundred generated coverage instances, verifies 1,024 retention-algebra identities, and compares the effective-reviewer formula with direct covariance calculations in 114 parameter settings.
The extension cross-check exhausts all forward rule subsets on three ordered nodes, every admitted-leaf set, every positive and negative observation set, and every node-covering patch family. An independent truth-table calculation checks feasibility and universal gluing. A separate enumeration compares encodings, task fibers, joint task partitions, and decoder composition on archive domains of at most four elements. These are bounded finite comparisons, not empirical models of mathematical practice.
The trace conformance suite adds independently enumerated finite models, canonical JSON records, and malformed or altered certificates. Its actual byte stream is processed by the Lean checker built in the current formal run. The report records each verdict and the exact input and output hashes. Rejection of a malformed record is not counted as a proof of an impossible mathematical request.
The general Lean proofs now establish the specified trace checker and typed codec. The Python producer, Python checker implementation, standard text parser, and source-address adapter retain separate conformance evidence.
The tests and cross-checks verify the implementation of finite definitions and examples. They do not replace the proofs in this monograph. Conversely, the proofs do not guarantee that a software implementation is free of defects. The release keeps both forms of verification.