C Reproduction and verification records
On this page · Permalink · Source line 2522
The package includes written proofs, exact finite producers and independent result checkers, and a fresh pinned Lean run. All eighteen modules were rebuilt and replayed. The mathematical imports remain cached and are not represented as freshly rebuilt dependencies. The current compiler record is evidence/formal_1.8.0/, while older evidence retains its original version. Source changes and the new mathematical environments are listed in the current progress ledger and publication report.
Before modifying the extracted package, check the delivered files:
python scripts/check_manifest.pyThen run the finite and publication checks:
python -m pip install -e ".[release]" --no-build-isolation
python -m pytest -o addopts='' -q
python scripts/deep_validation.py
python scripts/verify_bridge.py
python scripts/check_recovery_extension.py
python scripts/check_trace_exchange.py
python scripts/verify_publication_edition.pyRegenerate the exact figures with:
python scripts/design_figures.pyThe publication edition is 1.8.0 and the Python distribution is 1.6.0. This distribution adds a versioned trace-exchange codec, an independent indexed checker, and export/check commands without changing the existing named-field schema or provenance byte format. Its historical migration remains documented in docs/PROVENANCE_FORMAT.md. Installation may obtain build and numerical dependencies unless they are already supplied locally.
The manuscript can be rebuilt independently from docs/:
cd docs
pdflatex -interaction=nonstopmode -halt-on-error Proof_Path_Theory.tex
pdflatex -interaction=nonstopmode -halt-on-error Proof_Path_Theory.tex
pdflatex -interaction=nonstopmode -halt-on-error Proof_Path_Theory.texFormal and cross-language replay
On this page · Permalink · Source line 2557
A separate formal replay, with the pinned runtime already available, uses:
python scripts/verify_lean.py --runtime /path/to/portable-kitFor PowerShell, extraction precedes installation:
$zip = '.\Proof_Path_Theory_Monograph_1.8.0.zip'
Expand-Archive -LiteralPath $zip -DestinationPath '.\proof-path-release'
Set-Location '.\proof-path-release\Proof_Path_Theory_Monograph_v1.8.0'
python scripts/check_manifest.py
python -m pip install -e ".[release]" --no-build-isolation
python -m pytest -o addopts='' -qThe trace interface can be exercised without a Lean runtime:
proof-path wire-export examples/and_dag.json --negative B --output-prefix trial
proof-path wire-check trial.problem.json trial.certificate.jsonThe export writes the fixed indexed problem, the checked result, and the node/rule address book separately. The general AST theorem is in ProofPath.TraceWire. The executed byte adapter is formal/CheckTraceJson.lean; the fresh formal verifier runs it against the generated canonical exchange cases. The address book must still be checked against the intended source snapshot.
The dated report identifies the commands actually run. These checks do not supply independent peer review, universal software verification, or empirical validation of the social models. The redistribution-license decision remains open.