Repository navigation
FEP Formal 1.6.0 integrates a pinned review of OpenAI mathematics with portable mathematical methods, a substantially extended manuscript Supplement A, Lean statement analysis and reproducible visualizations.
The supplement connects the 168-topic catalogue to topology, law and parameter spaces, information geometry, statistics, control and thermodynamics. Result contracts name the carrier, assumptions, qualified theorem, witness and boundary example. Twelve upstream result units are reference comparisons; no upstream proof authority or runtime dependency is imported. Cross-corpus MDS compares 34 rows in 30 authored coordinates and discloses projection distortion and axis ambiguity. The 1,946 Lean declarations are lexical source analysis, rather than certified translations or dependency extraction.
Final source: d5387742ebe7e1c6e4591e78d190479433e82897. Full main CI completed successfully on that exact commit. Python: 2791 passed, 20 optional skips, zero failures/errors, 91.56% coverage; all eight required browser cases passed without skips. The fifteen Linux/macOS/Windows Python 3.10–3.14 installed-package cells passed. The final wheel separately passed all 17 API/CLI exports outside the checkout, exact package-resource comparison and nonmutation checks.
Lean 4.34.1 / Mathlib 4.34.1 verified all 168 canonical topic bodies with zero warnings, errors or sorry. The actual final 388-page manuscript passed the nine publication checks and independent cover, equation, figure, table, URI and privacy review. All 1,315 manuscript equations are numbered; Supplement A contains 55 equations, twelve cited figures and six captioned tables. The cover identifies Daniel Ari Friedman, Active Inference Institute, ORCID 0000-0001-6232-9096 and the canonical manuscript email.
Seven assets include the PDF, offline companion ZIP, wheel, sdist, exact tagged source ZIP, validation manifest and SHA-256 checksums. Extract the companion and open pdf/fep_lean_combined.pdf; its relative explorer link resolves to the included manuscript/assets/mathematical-map.html. The manifest distinguishes hosted, native, static, installed and manual evidence. Prior failed attempts and superseded candidate artifacts remain historical.
The manuscript is published as version DOI 10.5281/zenodo.23220027 under scholarly concept 19699233. The independently verified automatic GitHub software archive is published as software version DOI 10.5281/zenodo.23225872 under the separate software concept 23196891.
Compilation proves the exact selected Lean bodies and does not establish the Free Energy Principle as a physical theory. Semantic maturity remains separate. Frozen H3 primary execution, full seven-stage capture, the broader installed-status acceptance, Q7 generated-runner execution, optional Hermes/OpenGauss runs, empirical validation and current keyboard/accessibility/network acceptance for the new explorer remain governed research lanes. PR #44 requires a separately reviewed successor proof/source-custody epoch. This release does not claim those lanes are complete.