FEP_Lean v1.2.0 — connected Horizon research program

1.2.0 — 2026-09-17 — connected Horizon research program

Lean/Mathlib v4.34.0 toolchain program and pin cycle #7 (2026-09-15)

Commits (in order): ff5c712 bridge re-pin to GNN
e983de5e5c997d413a24c8af212d0d4a2ecf61a6 sealing the post-fa931c8
owner content; 88ffd01 toolchain bump of Lean/Mathlib to v4.34.0 (the
newest-stable gate demanded it: lean/lean-toolchain v4.33.1 → v4.34.0,
lakefile + lake-manifest re-resolved at mathlib 5ed29652) with the
155-topic FepSketches workspace migrated to the 4.34 Mathlib API, canonical
surfaces migrated and projections regenerated byte-identical,
lake build FepSketches at zero warnings, fep-lean verify at 155/155

Manuscript

• Review PDF: attached (fep_lean-manuscript-2026-09-17.pdf) — graphical-abstract cover, roster v18, publication-plane custody at this release's HEAD.

FEP_Lean v1.1.0 — 155-topic Lean 4 formalization catalogue

FEP_Lean v1.1.0 — 155-topic Lean 4 formalization catalogue

FEP_Lean v1.1.0 is the source-bound 155-topic publication cut of the Free
Energy Principle formalization catalogue. It spans 20 reviewed families in
five areas: the Free Energy Principle, Active Inference, Bayesian Mechanics,
Information Geometry, and non-equilibrium Thermodynamics.

• Immutable release DOI: 10.5281/zenodo.22072956
• Work-level concept DOI: 10.5281/zenodo.19699233
• Release commit: d7b6f8b15ea9dc451b191e3674a1fd72b5e586b4
• License: Creative Commons Attribution 4.0 International (CC BY 4.0)
• Release date: 2026-08-23

What changed

• Expanded the catalogue from 120 to 155 topics, with exact metadata,
  theorem-role closure, and composition witnesses across 20 families.
• Added finite-sample Laplace/Brier risk, closed-loop policy trees and treewise
  expected free energy, native conditional-independence/blanket transfer,
  finite exponential-family dual geometry, and exact two-state continuous-time
  Markov thermodynamics.
• Upgraded and pinned the formal workspace to Lean 4.33.1 and
  Mathlib 4.33.1, locked at Mathlib revision
  0df444a360eaa60ab8c11dca51a86af692955474.
• Expanded the typed numerical dashboard to 15 witnesses, the atlas to all
  155 topics / 20 families / 133 relations / 48 satisfied capabilities, and
  the manuscript to a reproducible 330-page publication.
• Hardened release provenance, browser replay, archive validation, Python
  acceptance receipts, manuscript rendering, metadata consistency, and
  fail-closed source/config/test binding.

Acceptance evidence

• Native Lean: 155/155 topic closures; 0 errors, 0 warnings, 0 sorry.
• Formal declaration/axiom audit: schema 4; 823 required formal-resource
  declarations, including 699 evidence declarations; no sorryAx and no
  untrusted project axioms.
• Python: 1,203 collected; 1,080 passed; 123 skipped; 0 failed/errors;
  89.81% line coverage (8,808/9,807 statements), above the unchanged 89% floor.
• Browser: schema-4 Chrome 151 replay; six source-bound screenshots; all
  155 topics, 20 families, 15 typed witnesses, 133 relations, and 48 satisfied
  capabilities represented.
• Reproducibility: two independently built 232-member evidence bundles are
  byte-identical at SHA-256
  0009447598ecd3bbf68548eab360704a2539480379791eb0128186fa230884ea.
  The wheel and canonically normalized source distribution are also
  byte-identical across two fresh build directories.

These checks establish the exact shipped formal statements and software
evidence. They do not prove the Free Energy Principle as a physical theory.
Provider-backed Hermes commentary is optional and unavailable for this release
cut; no historical provider report is promoted to current full-mode evidence.

Controlled assets

GitHub and Zenodo carry the same eight controlled files. The .sha256 files
contain the digest of their adjacent payload.

Asset	Bytes	SHA-256
fep-lean-1.1.0-155-evidence-bundle.tar.gz	6,095,784	0009447598ecd3bbf68548eab360704a2539480379791eb0128186fa230884ea
fep-lean-1.1.0-155-evidence-bundle.tar.gz.sha256	108	1dc08541ecf88b0666a77dd6305400fbe06a76594e3a2a38b381b63aebfc2c3d
fep-lean-manuscript-1.1.0.pdf	2,005,312	8fff9f892b5c3e6c1b579cfb774d59fc0e4c35ba771eaa558c73c946cd812fd4
fep-lean-manuscript-1.1.0.pdf.sha256	96	0d4e25730d127b96c43918db676d2cfbc5439202e23b8ea6d0bdce6fb94d8562
fep_lean-1.1.0-py3-none-any.whl	578,523	2d4f518999cd51f1147b12e13eae2c92f87848e64886c7df8c2a852e64746da7
fep_lean-1.1.0-py3-none-any.whl.sha256	98	5a435e7337b22463e47726fc3042f3ca9c007f34211636dce57a346c47678306
fep_lean-1.1.0.tar.gz	692,987	311a58f8c5fe5161e14302d07a702279055a64d4352204b6c4d4abbda4434fc3
fep_lean-1.1.0.tar.gz.sha256	88	e9ad6b76598357fba8bda1c2514001b122e0fa66523ee09a31aac7f1e169234d

The evidence bundle contains the source/config/test-bound receipts, rendered
HTML/PDF and renderer provenance, formalism atlas and numerical dashboard,
catalogue/manuscript projections, license, citation metadata, and a complete
per-member checksum manifest. GitHub-generated source archives are outside this
controlled eight-file parity set.

Reproduce and inspect

git clone https://github.com/ActiveInferenceInstitute/fep_lean.git
cd fep_lean
git checkout v1.1.0
uv sync --locked --extra dev
(cd lean && lake build FepSketches)
uv run python scripts/build_release_bundle.py --check \
  --output /path/to/fep-lean-1.1.0-155-evidence-bundle.tar.gz

See the repository README,
HANDOFF,
and the archived manuscript for exact evidence boundaries and extension points.

FEP_Lean v1.0.0 — Lean 4 Formalization of the Free Energy Principle

FEP_Lean v1.0.0 — Lean 4 Formalization of the Free Energy Principle

DOI: 10.5281/zenodo.19699234
License: Creative Commons Attribution 4.0 International (CC BY 4.0)
Copyleft: DAF 2026

Cite this release

Friedman, D. A. (2026). Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics. In Active Inference Journal. Zenodo. https://doi.org/10.5281/zenodo.19699234

What is inside

• 50-topic machine-checked catalogue spanning five theoretical pillars — FEP (14) · Active Inference (11) · Bayesian Mechanics (10) · Information Geometry (8) · non-equilibrium Thermodynamics (7).
• 50 / 50 sorry-free compilation under the pinned stack: Lean 4.29.0 + Mathlib 4.29.0 (lake env lean).
• Hermes / OpenGauss LLM-assisted pipeline with primary model moonshotai/kimi-k2.6, wall-clock deadlines, and a cache keyed to Lean source hashes; the Lean 4 kernel remains sole ground truth for every compilation claim.
• Zero-mock test discipline: 347 tests, ≥89 % combined line+branch coverage on src/, exercised against real files, a real SQLite store, live compiler invocations, and real HTTP round-trips.
• 168-page manuscript PDF (fep_lean_v1_04-24-2026.pdf, 1.82 MB) attached as a release asset.

Repository layout

• src/ — Python pipeline (catalogue, Hermes, verification, orchestrator).
• lean/ — Lake workspace with pinned toolchain and the 50-topic FepSketches module.
• manuscript/ — markdown chapters, references, figures, manuscript variables.
• tests/ — 347-test zero-mock suite.
• scripts/ — analysis + maintenance entry points.
• docs/ — API reference, configuration, troubleshooting, glossary.
• CITATION.cff — machine-readable citation metadata.
• LICENSE — CC BY 4.0.

Built from

This project is continuously re-verified from the docxology/template monorepo, which injects validated package- and manuscript-level metadata at render time.

Reproduction quick-start

git clone https://github.com/ActiveInferenceInstitute/FEP_Lean.git
cd FEP_Lean
uv sync --extra dev
uv run pytest tests/ --cov=src --cov-fail-under=89
bash scripts/_maint_bootstrap_lean_toolchain.sh   # Lean 4.29.0 + Mathlib 4.29.0
uv run python scripts/03_lean_verify_only.py      # native 50/50 sweep

---

© 2026 Daniel Ari Friedman · CC BY 4.0 · https://doi.org/10.5281/zenodo.19699234