Skip to content

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

Choose a tag to compare

View all tags
@docxology docxology released this 23 Aug 22:44
· 505 commits to main since this release
v1.1.0
d7b6f8b

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.

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.

Assets 10
Loading