# Full Text: Policy Entanglement in Active Inference: A Coupling-Parameter Deformation Framework for Multi-Stream Policy Posterior Distributions, Machine-Checked and Simulated with a Typed Float Boundary > Extracted from `Friedman_2026_Policy_ae7cdd62.pdf` --- ## Page 1 Policy Entanglement in Active Inference A Coupling-Parameter Deformation Framework for Multi-Stream Policy Posterior Distributions, Machine-Checked and Simulated with a Typed Float Boundary Daniel Ari Friedman Active Inference Institute daniel@activeinference.institute ORCID: 0000-0001-6232-9096 DOI: 10.5281/zenodo.20418904 Version 1.0 Active Inference Journal (2026) License: CC-BY-4.0 Policy Entanglement source repository May 27, 2026 ## Page 2 Contents Abstract 6 Part I — Introduction 6 Motivation and Position: Why Multi-Stream Active Inference Needs Parametric Policy Entangle- ment 7 The problem in plain language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Current coping strategies and their limits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Significance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Position relative to alternatives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 How the framework is developed: four parallel tracks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Reading guide . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Section dependencies (forward signposts) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Background and Prior Work: Antecedents in Active Inference, Variational Coupling, Information Geometry, and Tensor Networks 11 Discrete-time POMDP active inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Mean-field variational families and their limits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Hierarchical, deep, and sophisticated active inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Information geometry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Tensor networks and entanglement entropy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 KL / path-integral control and reinforcement learning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Multi-agent inference, Markov blankets, and renormalization . . . . . . . . . . . . . . . . . . . . . . . . . 14 Computational psychiatry and neural implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Lean 4, Mathlib, and formal verification of probabilistic systems . . . . . . . . . . . . . . . . . . . . . . . 15 Reproducible scientific software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Part II — Theory 15 Setup and Assumptions: Finite-Horizon Discrete POMDPs, Multi-Stream Policy Factorization, and the Mean-Field Baseline 16 Single-stream POMDP active inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 The multi-stream extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 The mean-field baseline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Lambda Deformation: Definition and Properties 17 Coupling potentials . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Definition: lambda-entangled policy posterior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 The coupling parameter lambda as a precision-like coupling weight . . . . . . . . . . . . . . . . . . . . . . 18 What J and K_c look like in practice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Entanglement Decomposition Theorem: Marginals, Coupling, and Total Correlation 19 Statement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Proof sketch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 What the decomposition says . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Optimal coupling: existence of lambda* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Takeaways . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Worked Examples: Bernoulli Toy, Motor-Attention Coupling, and Multi-Timescale Coupling 23 The K=2 Bernoulli toy: full closed form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Two-stream motor + attention with realistic EFE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Multi-timescale coupling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Information Geometry: Geodesics, Flatness, and Pythagorean Decomposition 27 Dual coordinates and the mean-field submanifold . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 The lambda-family is an e-geodesic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Connection to alpha-projections and curved exponential families . . . . . . . . . . . . . . . . . . . . . . . 33 Connection to escort distributions and deformed exponential families . . . . . . . . . . . . . . . . . . . . . 33 Takeaways . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ## Page 3 Spectral Structure: Schmidt Rank, Archetypal Decomposition, and Tensor-Train Bond Profiles 33 Bipartite Schmidt decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 The leading singular vectors as archetypal eigenvectors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Multi-stream tensor decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Birth and death of archetypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Takeaways . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Heterogeneous Inference: Mixed VFE/EFE Ensembles and the Coupling-Tax Bound 39 Three-level update hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Coupled marginal updates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 The VFE-only suboptimality bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Updating lambda: precision-like learning on coupling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Habit accumulation and revertibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Takeaways . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Phase Structure: Disordered, Mixed, and Frozen Coupling Regimes 42 Phase diagram . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Order parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Model predictions and behavioral hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Comparative Statics: Coupling Payoff, Two-Parameter Generalization, and Sensitivity Surfaces 44 The pay-off structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Two-parameter habit/EFE generalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Sensitivity to potential structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Part III — Formal Verification 47 What is proved . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 How the verification stack composes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Where to read the per-row content . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Lean 4 Formalization: Current Boundary, Witness Contracts, and Mathlib Scope 48 Current Lean artifact . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 What Mathlib4 is used for . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Mathlib4 analytic targets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Live-source injection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 What the Lean track proves today . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 The verification stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Validation gates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Part IV — Empirical Grounding 52 Empirical Simulation Suite: Bernoulli Validation, Coupling-Tax Envelope, Phase Diagram, and Spectral Structure 52 Two-stream Bernoulli (K=2) closed-form validation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Heterogeneous VFE / EFE coupling-tax bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Phase Structure of the 𝐾= 2 Ising Toy: Disordered, Mixed, and Frozen Regimes . . . . . . . . . . . . . . 54 Spectral structure (Schmidt rank, archetypes) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 Information-geometric structure (e-geodesic) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 Multi-stream coupling graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 𝐾> 2 ensembles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 Long-horizon rollouts and trajectory stationarity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 𝑚-projection revertibility witness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 Robustness and ablation stress tests . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 Software and numerical stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 Head-to-head BTAI baseline and adversarial-perturbation harnesses . . . . . . . . . . . . . . . . . . . . . 76 Anchored figure index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 pymdp 1.0.1 POMDP Harness: Architecture, Lambda Sweep, and Deterministic Rollout 78 Architecture: layered, not duplicated . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 The static 𝜆-sweep . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 Deterministic coupled rollout . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 2 ## Page 4 Anchored figure index for the pymdp harness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 pymdp Free-Energy Bundle Observables and Auto-Injected Summary Statistics 84 Statistical contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 Summary statistics across the sweep . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 Visualizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 Theorem 5.1 Numerical Witness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 Anchored figure index for the pymdp free-energy bundle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 pymdp Validation: Three-Tier CI Gates, Structured JSONL Run Log, and Bit-Reproducibility Contract 93 Three-tier validation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 Structured run log (JSONL) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 Software and source provenance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 Reproducibility contract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 Test budget snapshot . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 Part V — Connections to Existing Frameworks 95 Framework Connections I: pymdp/SPM Baseline, Hierarchical/Deep AIF, Sophisticated Infer- ence, and Branching-Time AIF 96 Relationship calculus for AIF variants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 Relation to recent unification efforts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 Mean-field active inference (pymdp, SPM, ActiveInference.jl) . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Hierarchical / Deep Active Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Sophisticated Inference (recursive EFE) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Branching-Time Active Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 Synthesis: How Every Connection Lands on Lambda, J, or Kc . . . . . . . . . . . . . . . . . . . . . . . . 99 Framework Connections II: KL/Path-Integral Control, Options Frameworks, Products-of-Experts, and Copula Variational Inference 100 KL / Path-Integral Stochastic Optimal Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 Options framework / Hierarchical RL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 Product of Experts and Mixture of Experts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 Copula variational inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 Recovery dictionary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 Framework Connections III: Multi-Agent Inference, RG-AIF Coarse-Graining, Markov Blankets, and CEREBRUM Case Grammar 102 Interactive Inference / Multi-Agent Active Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 Renormalization-group active inference (structural analogy) . . . . . . . . . . . . . . . . . . . . . . . . . . 103 Markov Blankets and Bayesian Mechanics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 CEREBRUM and case-grammar approaches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 Part VI — Discussion and Outlook 105 Open Theoretical Questions: Analytical Gaps, Identifiability, Empirical Frontiers, and Practical Research Directions 105 Where to start . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 How to read each question . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 Analytical questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 Identifiability and inference questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 Empirical questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Conceptual / cross-disciplinary questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Practical / formalization questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 Discussion and Outlook: Worldview, Live Artifact State, and Limitations 108 What the framework commits to . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 What the framework declines to commit to . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 The parametric-entanglement worldview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 Relation to the Free Energy Principle and active-inference process theory . . . . . . . . . . . . . . . . . . 109 3 ## Page 5 Six load-bearing properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 Live state of the artifact . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 Alignment and Dysregulation Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 Threats to validity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 Verification ledger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 Open directions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 Proof of the Entanglement Decomposition 113 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 Expanding the EFE expectation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 Expanding the prior log-expectation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 Combining . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 Interpretation (sign of 𝐼) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 Closed exponential-family form (collapsed identity) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 Convexity of Free Energy in Lambda: Conditions and Counter-Example 115 The closed exponential-family form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 The convexity ledger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 Sufficient condition for global convexity on [0, ∞) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 K = 2 Symmetric Ising specialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 Numerical verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 Complete Derivation: Two-Stream Bernoulli Toy 116 Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 Joint posterior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 Marginals (uniform by symmetry) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 Joint and marginal entropies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 Closed-form mutual information . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 Coupling from a target alignment (alignment-inversion, not a VFE optimum) . . . . . . . . . . . . . . . . 117 Free-energy curve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 Numerical cross-check . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 Tensor-Train Inference Algorithm: Bond-Dimension Sweep, MPS Contraction, and Sparsity-Rank Tradeoff 119 Tensor-train representation of J . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 The exponential map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 Inference cost . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 Sampling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 Marginal extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 Bond-dimension recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 Approximate compression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 Connection to the sparsity–rank tradeoff . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 Lean 4 Boundary Fragment: Live ActinfPolicyEntanglement Source Excerpts and Validation Wiring120 Package structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 Mathlib-free boundary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 Status snapshot . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 Building locally . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 FepSketches Re-exports for the Sibling fep_lean Layout . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 Where each manuscript theorem lives in Lean . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 The twenty live Lean companions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 Decomposition fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 Geometry fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124 Spectral fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 Convexity fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 Heterogeneous fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 Connections fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 Markov-blanket fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 How drift is prevented . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 4 ## Page 6 How a witness is consumed today . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 Notation Concordance: Symbol Registry Across Manuscript, LaTeX, Python, and Lean 128 How to read this concordance — one symbol, four tracks . . . . . . . . . . . . . . . . . . . . . . . . . 129 Sign conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 Sets, indices, and basic objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 POMDP generative-model symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 Distributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 Coupling potentials and parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 Information-theoretic quantities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 Free energies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 Manifolds, projections, and dual coordinates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 Spectral and tensor-network symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 Heterogeneous-ensemble quantities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 KL-control, copula, and product-of-experts symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 Relationship classes and claim-strength labels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 Hyperparameters (figure / sweep / simulation) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 LaTeX preamble macros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 Lean type abbreviations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 Phase / verdict labels (manuscript-level) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 Status notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 Conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 Common pitfalls when editing across tracks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 GNN fifth-track concordance (structural-and-numerical) . . . . . . . . . . . . . . . . . . . . . . . . . 138 Reference Tables: Claim Strength, Variant Recovery, Lean Inventory, pymdp Bundle Statistics, and JSONL Run-Log Schema 139 Claim-Strength Legend . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 Active-Inference Variant Recovery Ledger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 Lean 4 Boundary-Fragment Module Inventory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140 MathlibProofs ℝAnalytic Discharge Package: Inventory . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 pymdp Free-Energy Bundle: Auto-Injected Summary Statistics . . . . . . . . . . . . . . . . . . . . . . . . 143 Robustness and Ablation Stress-Test Ledger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 Evidence Ladder and Claim Provenance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 pymdp JSONL Run-Log Field Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 GNN as a Shipped Fifth Track: Triple-Play Mapping, a Verified K=2 Bernoulli Round-Trip, and a Lean Typed-Contract Emitter 146 Scope and Claim-Strength: a Shipped Bridge, with an Explicit Non-Claim About Proof . . . . . . . . . . 146 GNN Background: the Triple Play and the Active Inference Ontology . . . . . . . . . . . . . . . . . . . . 147 Acronym Disambiguation: GNN (Notation) vs. GNN (Graph Neural Network) . . . . . . . . . . . . . . . 147 Mapping the (𝐴, 𝐵, 𝐶, 𝐷, 𝐸, 𝐽, 𝜆) Tuple to a GNN Spec . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 Worked Example: the K=2 Bernoulli Toy as a Shipped GNN Round-Trip . . . . . . . . . . . . . . . . . . 148 What GNN Preserves and What It Abstracts Away . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 Shipped Elaboration: GNN to a Lean Typed-Structure Contract . . . . . . . . . . . . . . . . . . . . . . . 150 Shipped Round-Trip: GNN to pymdp Harness Configuration . . . . . . . . . . . . . . . . . . . . . . . . . 150 Downstream Use, Open Directions, and Open Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 Bibliography 152 Active inference and the free-energy principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 Branching-time and structured AIF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 Information geometry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 Information theory and multi-information . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 Variational and copula inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156 Variational inference robustness and Lipschitz bounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156 Tensor networks and quantum-inspired ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156 KL / path-integral control duality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 Control / RL as probabilistic inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 Hierarchical RL / options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 Markov blankets and particular physics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 5 ## Page 7 Computational psychiatry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 Integrated information / consciousness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 Multi-agent / interactive inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 Lean / formalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159 Software dependencies (companion code) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160 Scientific visualization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160 Abstract Active inference models often need to choose among several policy streams at once, for example streams tied to different effectors, sensory channels, agents, agents within a group, or planning horizons. Standard discrete active- inference implementations keep this manageable by treating those streams as independent, but that simplification removes the dependencies that make coordinated action possible. This manuscript introduces policy entanglement: a controlled deformation of the usual independent policy posterior by a scalar coupling strength and explicit compatibility and preference potentials. The construction preserves the finite active inference setting while making cross-stream dependence a first-class modeling object rather than an implicit artifact of the chosen factorization. The framework keeps a claim-strength ledger that distinguishes exact recoveries, parameterized embeddings, numerical witnesses, and structural analogies. Mean-field active inference is the exact independent case. Products of experts, copula variational inference, options, hierarchical and sophisticated inference, branching-time active inference, renormalization-style compression, and Markov-blanket multi-agent views are connected as special cases through their stated posterior-factorization maps. The central result is a free-energy decomposition that separates ordinary per-stream free energy, coupling preference terms, the coupling normalizer, and the information cost of leaving independence. The decomposition makes multi- information the explicit surcharge paid by a non-factorized policy posterior and shows how coupling strength, compatibility structure, and off-diagonal preference costs enter the same accounting identity. This result supplies the organizing principle for the rest of the paper. It supports an information-geometric reading of the coupled policy family as a path away from the mean-field submanifold, a projection identity that returns the coupled posterior to its independent marginals, a spectral and tensor-train view of dominant coordinated policy modes, a heterogeneous- ensemble coupling-tax bound, and a phase vocabulary for under-coupled, mixed, and highly concentrated policy posteriors. These interpretations are intentionally limited: the manuscript does not claim a neural, clinical, biological, or quantum implementation, and Markov-blanket and tensor-network language is used as scoped modeling analogy unless a specific theorem row or generated artifact supports a stronger statement. The main decomposition analytic identity is machine-checked in ℝin the Mathlib-backed Lean layer with an axiom audit and negative controls. A separate stock-Lean boundary fragment remains Mathlib-free and exposes the theorem surface as typed contracts for the Python simulation layer and the manuscript registry, including witness-consuming rows where analytic payloads are deliberately supplied at the boundary. The executable numerical layer remains a Float pipeline, so a verified Float↔ℝerror bridge is still an explicitly open interface rather than an implied proof; conservative interval brackets on the K=2 decomposition sweep certify Float residuals within a widened high-precision envelope (output/reports/float_real_residual.json) without promoting the registry row to proved. The empirical companion uses a partially observable Markov decision process (POMDP) simulation layer built with pymdp and NumPy to sweep coupled policy ensembles, run short and long rollouts, check the projection identity to round-off precision, produce free-energy, entropy, total-correlation, action-distribution, robustness, and adversarial sidecars, and render figures from those artifacts. The manuscript, figures, theorem map, citation registry, notation glossary (§S6), bibliography, and PDF are regenerated from the same source-owned pipeline, so prose claims are tied to Lean sources, Python witnesses, output metadata, and validation gates rather than maintained by hand. All manuscript methods, tests, and documentation are available as open-source software at https://github.com/ActiveInferenceInstitute/policy_entanglement (DOI: https://doi.org/10.5281/zenodo.20418904). Part I — Introduction This part frames the multi-stream policy-inference problem and surveys the prior work on which the framework builds. Two chapters: The Free Energy Principle enters this manuscript as a disciplined variational framing rather than as a slogan: adaptive systems can be modeled as maintaining tractable beliefs that bound sensory surprise, while active inference turns that variational bound into a process theory of perception, action, learning, and policy selection [Friston et al., 6 ## Page 8 2006, Friston, 2010, Buckley et al., 2017, Parr et al., 2022, Pezzulo et al., 2024]. That framing has also drawn careful scope critiques, especially around Markov blankets and the temptation to treat FEP as a theory of everything rather than as a modeling principle with explicit assumptions [Aguilera et al., 2022, Raja et al., 2021, Menary and Gillett, 2022]. The finite POMDP setting used here is therefore intentionally narrow: expected free energy supplies the policy objective, pymdp supplies a reproducible implementation substrate, and the contribution of this manuscript is to ask what happens when the policy posterior itself is allowed to carry explicit cross-stream dependence [Friston et al., 2017a, Parr and Friston, 2017a, Kaplan and Friston, 2018, Da Costa et al., 2020, Smith et al., 2022, Heins et al., 2022]. • §1 — why parametric coupling is needed. Real agents juggle many concurrent policy streams; strict mean-field factorization can discard cross-stream structure that is directly visible in the motivating examples of §1. A single tunable coupling parameter recovers strict factorization at one limit and arbitrary joint structure at the other. • §2 — what already exists in active inference, control theory, information geometry, and tensor networks that this framework relates to exactly, parametrically, or analogically. Eight axes of antecedents are surveyed (discrete-time POMDP AIF; mean-field variational families; hierarchical / deep / sophisticated AIF; information geometry; tensor networks; KL / path-integral control and RL; multi-agent inference and renormalization; formal verification and reproducible scientific software). The later recovery ledger separates exact recoveries (for example mean-field AIF and single-stream KL control) from parametric embeddings (for example explicit factor-graph policy factors, options, copula VI, and multi-agent coupling) and structural analogies (for example hierarchical, sophisticated, branching-time, renormalization-group, and Markov-blanket readings). The specific mappings are cataloged in §17 through §19. After Part I a reader has the motivating examples, the literature context, and the conceptual frame within which the analytical content of §3 onward is developed. Every symbol used in this manuscript is cataloged in §S6 across all four tracks (manuscript, LaTeX preamble, Python, Lean), with status notes flagging where a track diverges (e.g. unicode-vs-ASCII identifier conventions). The Lean track ships in two complementary packages: MathlibProofs/, which machine-checks the central S01 free-energy identity (Theorem 5.1) in ℝwith foundational- only #print axioms (propext, Classical.choice, Quot.sound; two independent negative controls audited on every build), and lean/ActinfPolicyEntanglement/, a stock-Lean v4.29.0 boundary fragment that ships the 21-row theorem surface as a typed API for the Python computational layer and the manuscript registry; §12 carries the per-row content table and docs/reference/veridical_status.md the running audit. Repository artifact. All four tracks (prose, equations, Python / pymdp, Lean 4) are maintained as a single working repository artifact [Friedman, 2026a]. The public Zenodo DOI (10.5281/zenodo.20418904) and source repository are recorded in manuscript/config.yaml and CITATION.cff. The entire build — rendered PDF, pymdp 1.0.1 numerical sidecars, dashboard invariants, and the MathlibProofs ℝ-level discharge — regenerates from a single command (./run.sh --pipeline or python scripts/run_all.py), and the repository’s machine-readable CITATION.cff provides the preferred citation form. Motivation and Position: Why Multi-Stream Active Inference Needs Parametric Policy Entanglement The problem in plain language Active inference furnishes a normative theory of a perceiving-and-acting unit by minimizing variational free energy across perception, action, and learning [Friston et al., 2006, Friston, 2010, Buckley et al., 2017, Friston et al., 2017a, Da Costa et al., 2020, Parr et al., 2022]. In the discrete-time POMDP formulation, a unit is specified by an observation likelihood 𝐴∶𝑝(𝑜∣𝑠), a transition tensor 𝐵∶𝑝(𝑠′ ∣𝑠, 𝑎), prior preferences over outcomes 𝐶, a prior over hidden states 𝐷, and a habit / prior over policies 𝐸(𝜋), where policies 𝜋live on a space of action- affordances replicated across a (possibly flexible) time horizon [Smith et al., 2022, Heins et al., 2022]. Expected free energy then gives each policy posterior both an epistemic term (seek observations that resolve uncertainty) and a pragmatic term (seek preferred outcomes), so action selection is not bolted onto perception but derived from the same variational calculus [Friston et al., 2017a, Sajid et al., 2021, Parr and Friston, 2019, Friston, 2018]. The formalism is mathematically compact, biologically motivated, and increasingly used across perception, decision-making, robotics, and computational psychiatry [Adams et al., 2013, Schwartenbeck and Friston, 2016, Lanillos et al., 2021], while its direct empirical status remains an active comparative-modeling question [Hodson et al., 2024]. An agent of any non-trivial complexity, however, is not best described by a single policy variable. A real agent 7 ## Page 9 juggles many concurrent policies: motor and attentional, fast and slow, modality-specific, with some streams treating the next move as a one-shot gradient descent on variational free energy (VFE) and others engaging in deep counterfactual planning under expected free energy (EFE). The standard discrete POMDP treatment in pymdp [Heins et al., 2022] and the continuous-state SPM-DEM lineage [Friston et al., 2008] split inference across independent factors and policies — that is, they rely on strict mean-field factorizations across hidden-state factors, observation modalities, and, in the multi-stream construction studied here, policy variables [Da Costa et al., 2020, Smith et al., 2022]. The mean-field separation is computationally cheap and biologically suggestive — it mirrors functional segregation, sparse cortical connectivity, and the modular character of much of the cortex — but it discards a structure that is visible in natural behavior and engineered agents: actions taken on one stream are routinely contingent on, anticipatory of, and instrumentally coupled to actions on others. A drummer’s left hand does not freely sample its policy distribution while the right hand plans the next fill; an autonomous vehicle’s lateral and longitudinal controllers share predictive structure with the symbolic route planner [Lanillos et al., 2021]; a human reaching for a cup while reading does not factor reach-policy and saccade-policy independently. Natural-task eye-tracking studies find that gaze typically arrives at the next task object before manipulation begins [Land and Hayhoe, 2001], and object-manipulation studies show hand shaping and grip forces coupled to visual sampling of the object [Johansson et al., 2001]. Contemporary world-model RL agents such as DreamerV3 [Hafner et al., 2023] give an adjacent machine-learning example: cross-modal predictive state is useful, but the architecture does not expose a scalar coupling parameter that the modeler can tune, infer, or validate. This document develops a tunable, analytically tractable, machine-checkable formalism for the parametric entangle- ment of concurrent policies in a single agent. The key move is structural rather than architectural: we do not commit to translation layers between symbolic planners and motor controllers (which would make the modeler responsible for the entire bridge), nor to fully joint enumeration of cross-modal policies (which combinatorially explodes), nor to hand-designed attention-gating that re-introduces the mean-field assumption at a higher level. We instead introduce a single tunable coupling parameter that interpolates between strict factorization and arbitrary joint structure, with a closed-form decomposition of free energy that exposes precisely what the entanglement buys. In FEP language, 𝜆 does not replace precision, preferences, or expected-free-energy minimization; it makes the strength of cross-stream policy dependence an explicit object that can be proved about, simulated, visualized, and validated. The phrase policy-posterior coupling is used narrowly. Standard active-inference notation already distinguishes posteriors over hidden states, policies, and parameters [Friston et al., 2017a, Smith et al., 2022]. This manuscript changes only the variational family for the policy posterior: the policy prior factors 𝐸𝑘, the expected-free-energy weights 𝛾𝑘𝐺𝑘, and the agent’s generative-model tensors remain visible, while 𝜆𝐽adds an explicit cross-stream factor on joint policy space. Thus 𝜆is not neural precision, not a new preference distribution, and not a biological measurement by itself; it is the scalar strength of a specified coupling potential inside the finite policy posterior. Current coping strategies and their limits The active-inference and probabilistic-modeling literatures have developed several strategies for handling cross- stream dependence on top of a mean-field backbone. Each is genuinely useful in its regime; each leaves a structural gap that the parametric construction below is designed to close. • Architectural translation layers. A common engineering pattern is to factor the agent into independent per- stream modules and hand-design a translation layer between them — for example, a symbolic-planner outputs a goal that a motor-controller consumes as a target. This decouples the modules at design time but moves the entire alignment problem into the translation layer, which is typically non-differentiable, non-Bayesian, and the implicit source of brittleness when the modules’ assumptions drift apart. • Hierarchical / deep active inference. Hierarchical AIF [Friston et al., 2017a, Pezzulo et al., 2018] organizes the agent into a stack of generative models with explicit message passing across levels. Within each level the mean-field assumption is re-imposed; cross-stream dependence is captured only through the bottleneck of the inter-level messages. When two streams at the same level depend on each other directly (left hand and right hand; saccade and reach), hierarchical AIF cannot express the dependence without inflating the level structure to a degree that loses biological plausibility. • Sophisticated inference. Sophisticated inference [Friston et al., 2021] introduces beliefs about beliefs through recursive expected free energy, capturing how an agent’s plan depends on what it will come to believe once an action is taken. This is a powerful generalization along the temporal axis but it does not address concurrent cross-stream coupling at a single decision point; the recursion is over future selves, not over peer streams. • Branching-time active inference. Branching-time AIF [Champion et al., 2022] expands the policy tree and prunes it with Monte Carlo tree search, allowing a much richer enumeration of joint futures. The price 8 ## Page 10 is computational: the policy space scales exponentially in horizon and arity, and the agent must spend search budget the framework does not give it any principled way to allocate. • Attention-gating and precision modulation. Dopaminergic precision learning [Friston et al., 2014, Schwartenbeck et al., 2015], the broader precision-in-action literature [Limanowski et al., 2024], and structured attention mechanisms [Hoffman and Blei, 2015] gate which streams influence the posterior at a given moment. This is well-suited to coarse on / off coupling but provides no continuous parameter for how strongly coupled the streams should be, nor any analytical decomposition of the cost paid for coupling. • Copula variational inference. Copula VI [Tran et al., 2015, Han et al., 2016] retains mean-field marginals and adds a parametric copula on top to model dependence. The construction is elegant in static settings but does not natively integrate with the EFE / planning side of active inference, and the choice of copula family is a non-trivial modeling commitment that does not interpolate smoothly to or from the mean-field baseline. • Tensor-network parameterized variational families. Tensor networks — matrix product states, tree- tensor networks, hierarchical Tucker decompositions [Han et al., 2018, Glasser et al., 2020, Verstraete et al., 2008, Eisert et al., 2010] — give compact structured joint distributions with controlled bond dimensions. We are not aware of a prior active-inference treatment that uses this exact tensor-network family as the policy posterior; one contribution of this manuscript is to show that the parametric coupling below is a tensor-network family in disguise, recovering MPS-style algorithmic structure as a side effect. Across these strategies, the diagnostic pattern is consistent: each one solves a piece of the cross-stream-coupling problem and leaves the remaining pieces to the modeler. A unified framework needs a single parameter that interpolates between strict mean-field and arbitrary joint structure, a closed-form bookkeeping for the cost of leaving the mean-field manifold, and a principled way to classify each neighboring strategy as an exact slice, a parametric modeling route, or a structural analogy. This placement also clarifies what the manuscript is not claiming. The framework is not a new general account of the Free Energy Principle, nor a replacement for the process theory of active inference. It is a focused extension of the variational family used for policy inference: the usual mean-field policy posterior remains the 𝜆= 0 anchor, while finite 𝜆represents a controlled departure from that anchor. The Markov-blanket and particular-physics literatures motivate why boundaries and conditional independences matter for self-organizing systems [Kirchhoff et al., 2018, Ramstead et al., 2018], and critical reviews warn that those ideas do not automatically license unrestricted biological or cognitive scope claims [Aguilera et al., 2022, Raja et al., 2021]. The claim tested here is narrower: within a finite- POMDP agent whose modeling boundary is already fixed, cross-stream policy dependence can be made a transparent mathematical and computational degree of freedom. Significance Six load-bearing properties of the framework: (i) Theoretical economy. The current AIF literature handles cross-stream coordination through a proliferation of architectural devices: branching-time tree search [Champion et al., 2022], hierarchical / deep AIF with explicit message passing [Pezzulo et al., 2018, Friston et al., 2017a,b], sophisticated inference with recursive EFE [Friston et al., 2021], and factor-graph forward-backward over multi-modal generative models [de Vries and Friston, 2017, Friston and Parr, 2017, Parr et al., 2019, van de Laar, 2019]. Part V classifies these relationships instead of flattening them into one claim: mean-field AIF is the exact 𝜆= 0 anchor; factor-graph message passing is a parametric implementation route whose inserted policy factor has exact semantics only inside the chosen graph; hierarchical, sophisticated, and branching-time AIF remain structural analogies unless their extra temporal or recursive machinery is explicitly built into 𝐽and the generative model. (ii) A clean decomposition theorem. §5 below gives a free-energy decomposition (Theorem 5.1) into (a) per- stream marginal free energies, (b) a coupling / partition-function bundle (𝛾𝜆⟨𝐾𝑐⟩, log 𝑍𝐸(𝜆), and −𝜆⟨𝐽⟩), and (c) the multi-information (total-correlation) term 𝐼(𝑞𝜆) ≥0 — see Eq. (5.2). The trade-off between coupling and correlation makes precise when “joint structure pays for itself” relative to mean-field baselines, where comparable accounts in the structured-VI literature [Saul and Jordan, 1995, Wainwright and Jordan, 2008, Hoffman and Blei, 2015] state the trade-off only implicitly. Three corollaries follow immediately: Corollary 5.2 (coupling-pays-for-itself verdict), Corollary 5.3 (mean-field reduction at 𝜆= 0), and Corollary 5.4 (strict gain when 𝑞is non-mean-field). (iii) Information geometry. The family {𝑞𝜆} is an exponential geodesic (e-geodesic) departing the mean-field submanifold, which is itself e-flat. This places the framework on the well-developed scaffolding of dually-flat statistical manifolds [Amari and Nagaoka, 2000, Amari, 2016, Nielsen, 2020], and connects revertibility (collapse to mean-field) to the canonical m-projection (taking marginals). Non-extensive analogs via escort / 𝜙-deformed exponential families [Naudts, 2011] generalize the construction to systems with non-extensive statistics. (iv) Spectral interpretation. For bipartite (𝐾= 2) couplings, the joint posterior 𝑞𝜆(𝜋1, 𝜋2) has a Schmidt decomposition; for 𝐾> 2, a Tucker or tensor-train decomposition. The leading singular vectors / Tucker factors 9 ## Page 11 are archetypal eigenvectors — the small number of dominant cross-stream behavioral modes that recur across instances of a habit. This is a direct probabilistic-graphical-model homologue of bipartite entanglement entropy in quantum many-body systems [Verstraete et al., 2008, Eisert et al., 2010, Han et al., 2018], and inherits all the favorable algorithmic structure of low-rank tensor decomposition. (v) Heterogeneous VFE/EFE ensembles. Many real agents are mixed: some streams are reflexive (one-step VFE descent) and others plan (EFE counterfactuals). §9 derives an 𝑂(𝜆2) suboptimality bound (Theorem 9.1) for VFE-only streams operating inside coupled ensembles. This formalizes a long-standing intuition: coupled reflexive controllers can ride along with planners up to a bounded coupling-norm tax (Corollary 9.2), providing a quantitative answer to “how reflexive can my low-level controllers be while still benefiting from higher-level planning?” (vi) Lean formalizability. The framework is built from objects (finite probability distributions, KL divergence, Shannon entropy, Bregman divergences) that are natural targets for Lean’s Mathlib [Community, 2020]. A prior line of work shipped a 50-topic Mathlib-checked FEP catalog and companion monograph [Friedman, 2026c]; here, §12 documents this manuscript’s two-package Lean architecture — a Mathlib4-backed MathlibProofs/ library that machine-checks the central decomposition (Theorem 5.1) in ℝwith foundational-only #print axioms, and a stock- Lean v4.29.0 ActinfPolicyEntanglement boundary fragment that ships the 21-row theorem surface as a typed API — reusing the same toolchain pin [de Moura and Ullrich, 2021] and re-export layout as that codebase. The boundary fragment is sorry / axiom / Mathlib-free and source-extracted into the manuscript prose; the per-row content table (§12) and the running audit at docs/reference/veridical_status.md document what each row certifies at the boundary versus what the Mathlib4 discharge layer establishes. Position relative to alternatives We make a deliberate choice not to take the embodiment-as-architecture route of solving the multi-policy problem by partitioning into hardware / software modules with explicit translation layers between symbolic reasoning and low-level control. That route has well-known costs: the translation layer becomes the entire alignment problem in microcosm, and it is non-differentiable. Instead, we take the parametric entanglement route: tunably couple the policy distributions themselves, leaving the structural distinction between modalities / timescales intact at the level of marginals while permitting arbitrary joint structure to emerge through a learned coupling potential. This is closest in spirit to: copula variational inference [Tran et al., 2015, Han et al., 2016], structured VI [Saul and Jordan, 1995, Wainwright and Jordan, 2008, Hoffman and Blei, 2015], product-of-experts compositions [Hinton, 2002], and tensor-network parameterized variational families [Han et al., 2018, Glasser et al., 2020] — but specialized to the policy-inference setting of active inference with explicit habit (𝐽), expected-free-energy (𝐺), and sophistication (𝛾). It also connects to KL / path-integral control [Kappen, 2005, Theodorou and Todorov, 2012], options frameworks [Sutton et al., 1999], multi-agent active inference [Maisto et al., 2024], and renormalization-group AIF [Friston et al., 2025]. Part V assigns each connection an exact, parametric, or analogical relationship class, so “connection” never has to mean “full recovery.” How the framework is developed: four parallel tracks The manuscript is unusual in that the same mathematical object is developed simultaneously on four parallel tracks (prose, equations, Python, Lean), each with its own primary literature, its own quality criteria, and its own role in the overall argument. The tracks are cross-referenced via a registry of injection tokens; a reader can enter on any track and land on any other in a single hop, and a CI validator fails the build on dangling tokens, hardcoded grid counts, seeds, or rollout horizons. • Prose (§3 onward). The natural-language presentation: definitions, theorem statements, proof sketches, worked examples, interpretive commentary. Every chapter in Part II opens with the objects under discussion and closes with a three-bullet Takeaways box that surfaces the load-bearing claims. Section numbering is owned by manuscript/refs/labels.yaml so that renumbering propagates everywhere automatically. • Formalism in equations (§4, §5, §7, §8, §9). Every load-bearing identity is a registered equation in the same labels file, auto-numbered as S.K and resolved through registry tokens so the manuscript’s mathematical structure can be traversed without ever encountering a hand-written equation number. The four foundational identities — the entanglement decomposition (Eq. (5.2)), the e-geodesic identity (Eq. (7.3)), the Pythagorean decomposition (Eq. (7.4)), and the 𝑂(𝜆2) coupling-tax bound (Eq. (9.2)) — anchor the rest. • Simulations on real pymdp agents (§14, §15). The empirical layer is not a re-implementation of pymdp’s mathematics; it instantiates real pymdp.agent.Agent objects [Heins et al., 2022] with the JAX backend [Bradbury et al., 2018], runs deterministic fixed-point-iteration inference, and reads off the resulting policy posteriors, expected free energies, and free-energy bundles for every 𝜆on the coupling sweep. The analytical 𝜆-coupling layer takes those pymdp outputs and adds the cross-stream term — so the simulation tracks exactly 10 ## Page 12 the deformation the theorems describe, not a stylized stand-in. At 𝜆= 0 the coupled joint is exactly the outer product of the pymdp per-stream posteriors; at finite 𝜆the joint concentrates on cross-stream archetypes that the bare pymdp run never sees. • Lean 4 companions in a real lake build environment (§12, §E). The formal track is a Lean 4 boundary fragment under ../lean/ that compiles against stock Lean v4.29.0 [de Moura and Ullrich, 2021] with no Mathlib dependency, zero strict sorrys, zero axioms beyond stock Lean, and no unsafe / partial / noncomputable declarations. Every theorem in the body that admits a witness-form statement (including Theorem 5.1) has a Lean companion that actually compiles in the project’s lake build; its source is auto- extracted in the theorem sections and appendix via registry Lean tokens. The witness-form discipline makes the analytic-content boundary explicit: Mathlib4 is used in the manuscript as the named library context for those analytic obligations, while the current source blocks remain exactly the code that builds today. The four-track contract is not aspirational; it is CI-gated. The cross-reference and hyperlink test suites under ../tests/test_token_resolution.py and ../tests/test_project_wide_hyperlinks.py fail the build if any [[SECREF:]], [[THMREF:]], [[LEAN:]], [[VAR:]], [[FIG:]], or markdown link does not resolve, so a reader who finds a dangling reference has discovered a bug rather than an omission. Reading guide The manuscript has three logical layers; readers can profitably enter at any of the three depending on background. Choose the conceptual path if the question driving you is “why does multi-stream coupling matter and what does it look like when an agent does it well?”; choose the analytical path if you want to verify the load-bearing mathematical claims and follow the proofs; choose the empirical path if you want to reproduce every numerical result against the pymdp-grounded harness and inspect the JSONL run log. • Conceptual / qualitative path. This section (§1) →§3 (POMDP recap) →§4 (the parametric deformation) →§6 (worked toys) →§10 (phase regimes) →§21 (worldview). No proofs required; the closed-form K=2 Bernoulli derivation is the fastest entry point to the mathematics. • Analytical / theorem path. §5 (Theorem 5.1, the load-bearing identity) →§7 (e/m-flatness, e-geodesic, Pythagorean) →§8 (Schmidt rank, archetypes, tensor-train) →§9 (the 𝑂(𝜆2) coupling-tax bound, Theorem 9.1) →§11 (comparative statics). • Empirical / reproducibility path. §13 (closed-form Bernoulli + heterogeneous tax + phase + spectral) →§14 (1.0.1 architecture) →§15 (the free-energy bundle and derived summary statistics) →§16 (validation gates + JSONL run log + reproducibility contract). The Lean formalization plan (§12, §E) is orthogonal to all three paths and can be read at any point; every registered theorem in this manuscript names its Lean companion so a reader can navigate prose →theorem-statement →Lean- source in one hop. A single notation glossary (§S6) consolidates every symbol — including manuscript / LaTeX / Python / Lean counterparts — so prose that introduces new symbols can always be cross-referenced without ambiguity. Section dependencies (forward signposts) Builds on Used by §3 every later section §4 §5, §6, §7, §8 §5 (Theorem 5.1) §6, §11, §10 §7 (Theorem 7.4, Proposition 7.5) §8, §9, §17 §8 (Proposition 8.1) §10, §19 §9 (Theorem 9.1) §11, §13 §13 §14, §15, §16 §14 §15, §16 Background and Prior Work: Antecedents in Active Inference, Varia- tional Coupling, Information Geometry, and Tensor Networks This chapter catalogs the lines of work the framework builds on and points to where each one returns in the body. Detailed comparisons live in Part V (§17, §18, §19). This chapter provides the substantive orientation required 11 ## Page 13 for the body of the paper. The eight subsections below mirror eight axes of structural commitment: a Markov- decision substrate, a variational family, hierarchical / sophisticated extensions, an information-geometric ambient, a low-rank algorithmic backend, a control-theoretic and reinforcement-learning dual, multi-agent / renormalization analogies, and a formal-verification plus reproducible-software scaffold. Clinical and neural language is treated here as hypothesis-generating context, not as diagnostic evidence. Discrete-time POMDP active inference The discrete-time POMDP formulation of active inference is the home setting throughout. The standard treatment combines a generative model (𝐴, 𝐵, 𝐶, 𝐷, 𝐸) with planning-as-inference under expected free energy [Friston, 2010, Friston et al., 2014, 2017a, Kaplan and Friston, 2018, Smith et al., 2022, Sajid et al., 2021, Parr et al., 2022], introducing policies as random variables over which the agent maintains a posterior shaped jointly by past observations and anticipated outcomes. Recent unification and agency-formalization work further clarifies how multiple expected-free-energy formulations can be derived from shared roots, how EFE-based planning may be recast as variational inference, and how active inference can be used as a model-comparison language for agency [Champion et al., 2024, de Vries et al., 2025, Nuijten and Lukashchuk, 2025, Da Costa et al., 2024]. That literature is not purely consolidating: Millidge, Tschantz, and Buckley analyze where EFE derivations diverge, so this manuscript treats each per-stream 𝐺𝑘as a specified modeling choice rather than a unique consequence of FEP [Millidge et al., 2021]. Implementations now span several software lineages: pymdp targets open-source discrete state-space active inference in Python [Heins et al., 2022], RxInfer.jl supplies reactive variational message passing for real-time Bayesian inference in Julia [Bagaev and Podusenko, 2023], ActiveInference.jl provides Julia tooling for POMDP active-inference simulation and parameter estimation [Nehrer et al., 2025], and SPM-DEM remains the continuous-state dynamic-expectation- maximization ancestor [Friston et al., 2008]. The present manuscript’s empirical harness is built directly against pymdp 1.0.1 (§14), while the mathematical recap in §3 and the Lean recap in §12 keep the same generative-model schema explicit. Within that lineage, expected free energy is the point at which epistemic and pragmatic control meet: policies are preferred when they both reduce expected uncertainty and realize prior preferences. Cognitive-consistency interpretations make the same split visible in psychological language: epistemic and motivational closure are coupled but not identical objectives [Friston, 2018]. This is why policy coupling is not a cosmetic addition. If two policy streams share epistemic opportunities or pragmatic costs, strict factorization can erase precisely the joint structure through which the process theory expresses coordinated action; epistemic-value and navigation examples make that risk concrete in ordinary active inference before any coupling extension is added [Parr and Friston, 2017a, Kaplan and Friston, 2018]. The action-oriented-model-learning literature makes the same pressure visible from another angle: agents need models that are parsimonious because they are oriented toward possible action [Tschantz et al., 2020]. Here the parsimonious object is the coupling potential 𝐽and its scalar strength 𝜆, rather than an additional hidden-state factor or hand-designed controller interface. Factor-graph and graphical-brain accounts show how generative-model structure induces message-passing schedules [de Vries and Friston, 2017, Friston and Parr, 2017], and approximation-family work distinguishes mean-field, Bethe, and marginal message passing as different commitments about how local beliefs compose [Parr et al., 2019, Yedidia et al., 2005]. The word “free energy” is doing different work across those lineages: Bethe / Kikuchi free energies govern approximate marginal inference on factor graphs, while active inference adds policy selection, preferences, and epistemic terms. In the present manuscript, an additional policy factor can implement the 𝜆-coupling inside a chosen graph; the exactness belongs to that chosen graphical model, not to active inference in the abstract. The standard discrete-POMDP treatment commits to one policy random variable per agent, or to a factorized family of per-factor policy posteriors when the model is decomposed. That design is tractable, but multi-stream coordination is then carried by the modeling factorization rather than by an explicit coupling object [Da Costa et al., 2020, Smith et al., 2022]. This commitment is the entry point for the parametric coupling introduced in §4. Mean-field variational families and their limits Mean-field factorization is the workhorse approximation of variational inference and its active-inference instantiation: factorize the joint posterior across hidden-state factors, observation modalities, and policy variables to make the per-factor updates tractable [Wainwright and Jordan, 2008, Blei et al., 2017, Da Costa et al., 2020, Smith et al., 2022]. The cost is well known and well-studied: Hoffman and Blei note that the independence approximation “limits the fidelity” of the approximation [Hoffman and Blei, 2015], while Blei, Kucukelbir, and McAuliffe present mean-field and structured variational families as choices in an optimization problem rather than as exact posterior semantics [Blei et al., 2017]. In the present setting, any genuine cross-factor dependence is discarded, and the magnitude of the resulting bias is measured by the multi-information between factors — the same quantity that appears as the surcharge in Theorem 5.1. The point is not that mean-field is wrong; it is that mean-field lacks an internal observable 12 ## Page 14 for the dependence it has projected away. Three lines of prior work attempt to relax mean-field while preserving tractability: • Structured VI preserves selected dependency substructures while approximating the remaining interactions [Saul and Jordan, 1995, Wainwright and Jordan, 2008, Blei et al., 2017], and structured stochastic VI [Hoffman and Blei, 2015] introduces dependence between subsets of variables via amortized sub-models with shared parameters, capturing coarse-grained dependencies at the cost of additional architectural commitment. • Copula variational inference [Tran et al., 2015, Han et al., 2016] inserts a parametric copula on top of the mean-field marginals, preserving the per-stream factor structure and confining dependence to the copula density in the classical copula sense [Nelsen, 2006]. • Tensor-network parameterized variational families [Biamonte and Bergholm, 2017, Cichocki et al., 2016, Han et al., 2018, Glasser et al., 2020] use matrix-product-state and tree-tensor-network factorizations as compact joint distributions, importing algorithmic infrastructure from tensor-network physics and numerical multilinear algebra [Verstraete et al., 2008, Eisert et al., 2010, Orus, 2014]. The framework here is a parametric interpolation across all three: 𝜆= 0 recovers strict mean-field; finite 𝜆 with appropriate 𝐽realizes products of experts exactly, copula VI parametrically, and tensor-network variational structure as the algorithmic backend for low-rank coupling (§18). Crucially, these are structural correspondences, not benchmark claims: at each exact or parametric specialization the entanglement decomposition of Theorem 5.1 reduces by substitution to the relevant variational-free-energy expression. Where the relationship is only analogical, such as renormalization-group AIF, the recovery dictionary marks it as analogical rather than exact. Hierarchical, deep, and sophisticated active inference Hierarchical / deep active inference [Friston et al., 2017a,b, Pezzulo et al., 2018] decomposes the agent into a hierarchy of generative models with explicit message passing across levels — a treatment that captures temporally-extended structure and cortically-plausible scale separation [Friston et al., 2025], but that retains the mean-field assumption within each level. Sophisticated inference [Friston et al., 2021] introduces beliefs about beliefs through recursive expected free energy, modeling how an agent’s plan depends on the beliefs it anticipates having after taking an action. Branching-time AIF [Champion et al., 2022] addresses the exponential cost of policy enumeration via Monte Carlo tree search applied to the EFE tree. Each motivates a different structural choice, but none should be read as a full exact recovery in the current artifact. Hierarchical AIF corresponds to block-bidiagonal 𝐽as a cross-level concentration witness (Theorem 17.1), while temporal-scale separation and directed top-down / bottom-up message passing remain part of the source process theory. Sophisticated inference embeds with recursion-depth-many streams and a belief-about-belief 𝐽(Proposition 17.2), while the recursive observation-conditioning is a constraint on how that 𝐽is supplied. Branching-time AIF suggests tensor-train or prefix-tree compression of 𝑞𝜆, but the present manuscript does not run a head-to-head BTAI algorithmic comparison. The detailed mappings are tabulated in §17 and the appendix recovery ledger. Information geometry Dually-flat statistical manifolds, 𝑒- and 𝑚-coordinates, 𝛼-projections, and Bregman divergences are the natural language for parametric extensions of variational families [Amari and Nagaoka, 2000, Amari, 2016, Nielsen, 2020, Ay et al., 2017]. The 𝜆-deformation lives on this scaffolding: {𝑞𝜆} is an 𝑒-geodesic (Theorem 7.4), the mean- field submanifold is 𝑒-flat (Proposition 7.1), and revertibility (collapse to mean-field marginals) is the canonical 𝑚-projection (Proposition 7.2). The Pythagorean decomposition (Proposition 7.5) provides an exact split of the KL from the entangled posterior to any reference distribution into a multi-information term and a marginal-to-reference KL. Non-extensive generalizations via Tsallis / Rényi entropies and escort distributions [Naudts, 2011] yield 𝜙-deformed exponential families on which the same construction goes through with quantitatively different geometry; we flag the 𝑞-deformed analog as a natural extension (§7.4) without developing it here. Information geometry also supplies vocabulary used in integrated-information studies of consciousness [Tononi, 2008], but the present framework makes only a policy-space analogy: total correlation and low-rank structure quantify dependence among policy streams after the modeling boundary is fixed. It does not claim to solve consciousness, define phenomenology, or validate an integrated-information theory. Tensor networks and entanglement entropy Schmidt decomposition, matrix-product states, and the area law of entanglement entropy [Verstraete et al., 2008, Eisert et al., 2010] supply both the algorithmic backend and the conceptual vocabulary for the spectral structure 13 ## Page 15 of entangled posteriors. General tensor-network surveys and machine-learning treatments supply the computational bridge from that physics vocabulary to low-rank tensor representations of high-dimensional arrays [Biamonte and Bergholm, 2017, Cichocki et al., 2016, Orus, 2014]. In the bipartite (𝐾= 2) case the joint 𝑞𝜆(𝜋1, 𝜋2) admits a Schmidt decomposition whose leading singular vectors are the archetypal eigenvectors — the few dominant cross- stream behavioral modes (§8). For 𝐾> 2 a tensor-train factorization with bond-dimension profile (𝑟1, … , 𝑟𝐾−1) controls representational capacity (Proposition 8.1, §D). The tensor-network perspective also gives the framework its sharpest computational claim: low-rank coupling potentials produce low-rank posteriors (Theorem 8.3, the sparsity-rank tradeoff), making structured-coupling inference scalable in the bond dimension rather than in the raw policy-space size. The tensor-network literature has independently developed efficient inference algorithms — DMRG, TEBD, MERA [Han et al., 2018, Glasser et al., 2020, Schollwöck, 2011] — that become available once a coupling potential is represented in a tensor-network form; the present artifact demonstrates the rank/bond-profile side of that claim through the multi-𝐾sweep and tensor-train figures, while full tensor-network inference is left as an algorithmic extension. Categorical-systems- theory formulations of structured active inference [Smithe, 2024] further suggest that the same compositional vocabulary admits formal-verification-amenable presentations of structured policies. All tensor-network language in the manuscript is therefore a probability-tensor and linear-algebra analogy. It is not a claim that policy streams are quantum subsystems, or that quantum entanglement semantics are being imported into active inference. KL / path-integral control and reinforcement learning KL / path-integral control duality [Kappen, 2005, Todorov, 2006, Theodorou and Todorov, 2012, Rawlik et al., 2013] formalizes the equivalence between stochastic optimal control and free-energy minimization: the value function under a controlled stochastic system is the log-partition of an unnormalized path measure weighted by exponentiated cost. The options framework / hierarchical RL [Sutton et al., 1999, Barto and Mahadevan, 2003, Bacon et al., 2017, Doll et al., 2015] decomposes long-horizon RL into reusable temporally-extended sub-policies with explicit initiation / termination structure. Both fit cleanly into the parametric construction when the required factors are supplied: KL control corresponds to the special-purpose choice in which 𝜆𝐽is the negative control-effort cost (single-stream limit); options correspond to an option-like two-stream factorization with 𝐽encoding option-membership structure (§18). A subtler connection is to products of experts [Hinton, 2002]: the 𝜆-entangled prior ℰ𝜆(𝜋) = ∏𝑘𝐸𝑘(𝜋𝑘) 𝑒𝜆𝐽(𝜋) is literally a product of experts on joint policy space, with the coupling potential acting as one additional expert that only fires on configurations where the cross-stream relationship holds. Multi-agent inference, Markov blankets, and renormalization Interactive / multi-agent active inference [Maisto et al., 2024] models multi-agent cooperation as joint inference under shared generative models, while collective active-inference models show how group-level coordination can arise from surprise minimization under coupled generative models [Heins et al., 2024]. Renormalization-group AIF [Friston et al., 2025] derives hierarchical generative models via repeated application of a coarse-graining operator that preserves dynamics-form. Bayesian-mechanics treatments of Markov blankets [Friston, 2019, Da Costa et al., 2021] identify a system with a partition of states into internal / external / blanket, while Markov-blanket accounts of autonomy emphasize that a system boundary is an inferential and conditional-independence structure rather than just a physical envelope [Kirchhoff et al., 2018, Ramstead et al., 2018]. The critical literature is important here: both technical and philosophical reviews argue that Markov blankets require careful modeling assumptions and do not, by themselves, settle the scope of FEP, active inference, or cognitive boundaries [Aguilera et al., 2022, Raja et al., 2021, Menary and Gillett, 2022]. All three relate to 𝑁𝐾-stream entanglement only after the modeling boundary and coupling graph are specified. Multi-agent inference is a parametric joint-policy prior when within-agent and across-agent blocks of 𝐽are added to a shared or linked generative model. Renormalization-group AIF is an analogy between coarse-graining and low-rank policy-posterior projection. Markov-blanket separation is a policy-space analog quantified by normalized multi-information (§19), not a recovery of the state-space blanket construction. The manuscript therefore does not infer new biological boundaries from 𝐽; it supplies a way to measure and manipulate policy dependence once a modeling boundary has already been chosen. Computational psychiatry and neural implementation Computational-psychiatry programs use AIF to model dysregulation of perception, action, and learning [Adams et al., 2013, Schwartenbeck and Friston, 2016], often associating symptom dimensions with failure modes of the free- energy-minimization machinery (sensory precision dysregulation, prior over-weighting, habit rigidity). Dopaminergic / policy-precision accounts [Friston et al., 2014, Schwartenbeck et al., 2015, Parr and Friston, 2017b] and recent 14 ## Page 16 precision-in-action reviews [Limanowski et al., 2024], together with empirical precision-weighting evidence in psychosis [Haarsma et al., 2021], motivate the precision vocabulary, but the present framework borrows only the formal precision analogy for 𝜆(§9.4). It does not identify 𝜆with dopamine, synaptic gain, or any specific neural variable. The phase-structure analysis in §10 flags a coupling-drift failure mode (under- or over-coupling of behavioral streams) that is qualitatively distinct from per-stream prior corruption. We treat the clinical language as a model-generated hypothesis, not a diagnostic claim: if the coupling account is right, controlled tasks would be expected to reveal cross-stream covariance signatures (joint-action repertoire, between-trial mode statistics, coupling-spectrum effective rank) that are not visible in per-stream marginal measures alone. This is consistent with the habit-vs-deliberation balance literature [Doll et al., 2015] while adding an explicit coupling parameter that a follow-up empirical protocol could estimate. Lean 4, Mathlib, and formal verification of probabilistic systems Lean 4 [de Moura and Ullrich, 2021, FRO, 2026a] and the Mathlib library [Community, 2020, FRO, 2026b] are the formal-verification backbone of the present work. Lean 4 is a dependently-typed proof assistant with a minimal trusted kernel and a tactic framework expressive enough to mechanize contemporary mathematics; Mathlib provides — among many other things — the measure theory, linear algebra, and analysis targeted by the separate additive discharge of the framework’s witness-form theorems. A prior line of work shipped a 50-topic Mathlib-checked FEP catalog and companion monograph [Friedman, 2026c]; the present manuscript’s ActinfPolicyEntanglement boundary fragment (§12, §E) reuses the same toolchain pin and re-export layout, with witness-form theorems isolating the analytic content for a separate Mathlib4 discharge layer. Every numbered theorem in this manuscript — including the spectral semicontinuity and tensor-train rank claims of §8 (Proposition 8.2, Theorem 8.3) and the hierarchical / sophisticated-inference embeddings of §17 (Theorem 17.1, Proposition 17.2) — now carries a live Lean companion in that fragment. The choice to keep the present fragment Mathlib-free is deliberate: it forces every theorem statement to be expressible in the in-house CommScalar α typeclass, exposes the analytic content as explicit witness arguments, and makes the boundary’s hygiene budget (zero strict sorry, zero axioms, zero unsafe / partial / noncomputable) easy to verify against stock Lean v4.29.0. The verified-numerics boundary remains separate from this proof story. Numerical analysis supplies the right vocabulary for round-off, conditioning, and stability [Higham, 2002], while IEEE 754 fixes the floating-point arithmetic standard a formal bridge would have to model [IEEE, 2019], and proof-assistant floating-point libraries such as Flocq show what such a bridge requires [Boldo and Melquiond, 2011]. The present artifact machine-checks the exact ℝmathematics and tests the Float pipeline to strict tolerances; it does not claim a formal Float↔ℝ theorem. Reproducible scientific software The empirical layer is built on NumPy [Harris et al., 2020], SciPy [Virtanen et al., 2020], JAX [Bradbury et al., 2018] (which underpins pymdp 1.0.1), and Matplotlib [Hunter, 2007]. Every numeric value in the manuscript flows from a real run via the [[VAR:]] token system (§16); every figure carries reproducibility tEXt metadata (source script, function, hyperparameter snapshot, git revision, ISO timestamp, and compact plotted-data summaries); every cross-reference resolves through the same registry that the renderer consumes. This positions the manuscript inside the broader open-science / reproducible-research practice and — concretely — makes the manuscript an executable artifact: running scripts/run_all.py regenerates every numeric, every figure, and every theorem-table row from a single deterministic pipeline. Part II — Theory The mathematical core of the manuscript. Each chapter introduces the objects, states the load-bearing theorems about them, and immediately gives the proof or proof sketch (full proofs in the supplements). The chain proceeds: 1. §3 — discrete-time POMDP active inference and the mean-field baseline against which everything is measured. 2. §4 — the parametric coupling construction: 𝐽(habit) and 𝐾𝑐(preference) potentials, and the 𝜆-entangled posterior they define. 3. §5 — the load-bearing identity (Theorem 5.1) splitting free energy into marginals, coupling, and a non-negative multi-information term. 15 ## Page 17 4. §6 — three worked cases (Bernoulli closed form, motor-attention, multi-timescale) that make the abstract machinery concrete. 5. §7 — dual e/m information geometry; the 𝜆-family is an e-geodesic (Theorem 7.4); Pythagorean decomposition (Proposition 7.5). 6. §8 — Schmidt rank (Proposition 8.1), archetypal eigenvectors, tensor-train bond dimensions (Theorem 8.3). 7. §9 — VFE/EFE mixed ensembles and the 𝑂(𝜆2) coupling-tax bound (Theorem 9.1). 8. §10 — disordered / mixed / frozen coupling regimes and their behavioral signatures. 9. §11 — sensitivity, two-parameter generalization, potential-structure dependence. Every theorem in this part carries a Lean companion (see the per-row status in docs/reference/veridical_status.md) and a Python numerical witness (see docs/reference/_theorem_map.md). The supplements (§A, §B, §C, §D) carry the full derivations. Setup and Assumptions: Finite-Horizon Discrete POMDPs, Multi- Stream Policy Factorization, and the Mean-Field Baseline We work throughout with finite, discrete state and action spaces — adequate for the analytical results, computation- ally tractable, and aligned with the discrete-time POMDP formulation that dominates AIF practice (pymdp, RxInfer, ActiveInference.jl, SPM-DEM) [Heins et al., 2022, Bagaev and Podusenko, 2023, Nehrer et al., 2025, Friston et al., 2008]. Continuous extensions are sketched in §21. Every symbol introduced here also appears in the unified notation glossary (§S6) with its LaTeX, Python, and Lean counterparts. Single-stream POMDP active inference A standard discrete POMDP active inference unit: Symbol Meaning 𝑠∈𝒮 hidden state (finite) 𝑜∈𝒪 observation (finite) 𝑎∈𝒜 action (finite) 𝜋∈Π policy: sequence/map of actions over horizon 𝑇 𝐴𝑖𝑗= 𝑝(𝑜= 𝑖∣𝑠= 𝑗) likelihood matrix 𝐵𝑎 𝑖𝑗= 𝑝(𝑠′ = 𝑖∣𝑠= 𝑗, 𝑎) transition tensor 𝐶(𝑜) = log ̃𝑝(𝑜) log-prior preferences 𝐷(𝑠) = 𝑝(𝑠0) initial state prior 𝐸(𝜋) habit / policy prior on Π 𝛾 policy precision Under planning-as-inference with expected free energy [Friston et al., 2014, Da Costa et al., 2020]: 𝑞(𝜋) ∝𝐸(𝜋) exp( −𝛾𝐺(𝜋)), 𝐺(𝜋) = Risk(𝜋) + Ambiguity(𝜋) (3.1) with the standard EFE decomposition into pragmatic and epistemic components 𝐺(𝜋) = 𝔼𝑞(𝑜,𝑠∣𝜋)[ log 𝑞(𝑠∣𝜋) −log 𝑝(𝑠∣𝑜, 𝜋)] ⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟ epistemic value, negated + 𝔼𝑞(𝑜∣𝜋)[𝐷KL(𝑞(𝑜∣𝜋) ‖ ̃𝑝(𝑜))] ⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟ pragmatic value, negated . (3.2) (Sign conventions for 𝐹, 𝐺, 𝐾𝑐are cataloged in §S6.1; the “negated” annotations above match the standard EFE convention there.) VFE-only streams are obtained by treating 𝐺as an immediate variational objective (no recursive lookahead), where action selection is the gradient step on 𝐹at the current belief; the policy distribution effectively collapses to a delta on the next-action argmin. In planning-as-inference with 𝛾moderate, 𝑞(𝜋) remains a proper distribution over the policy space. Having fixed the single-stream POMDP baseline, we now generalize to the multi-stream setting that is the substantive subject of this manuscript. 16 ## Page 18 The multi-stream extension We posit 𝐾concurrent policy variables 𝜋= (𝜋1, 𝜋2, … , 𝜋𝐾), 𝜋𝑘∈Π𝑘, Π = 𝐾 ∏ 𝑘=1 Π𝑘. (3.3) Generic streams. The 𝐾streams are generic in three independent senses, all of which the framework handles uniformly: • Modality. Each stream may correspond to a distinct observation modality (visual, auditory, proprioceptive) and/or distinct hidden-state factor (location, identity, intent). • Time horizon. Streams may differ in planning horizon 𝑇𝑘— a fast attentional policy and a slow navigational policy are simultaneously representable without forcing them onto a shared clock. • Inference mode. Each stream may use VFE-only, EFE-planning, or sophisticated inference (recursive EFE; [Friston et al., 2021]). Concretely: a drummer’s left-hand timing stream (motor modality, short horizon, reflexive VFE) co-exists with a right-hand fill-planning stream (motor modality, longer horizon, EFE planning); an autonomous vehicle couples a very short-horizon steering controller (proprioceptive, VFE) with a much longer-horizon route planner (symbolic, EFE) and an intermediate-horizon attention allocator (visual, EFE); a reading-while-reaching agent factors immediate saccade policy (visual, VFE) from short-horizon reach policy (proprioceptive, EFE). In each example the streams differ along at least two of the three axes above, and the coordination between them is precisely what the entanglement framework formalizes. Let 𝒱⊆{1, … , 𝐾} index VFE-only streams and 𝒫= {1, … , 𝐾} ∖𝒱index planning streams. The heterogeneous- ensemble pay-off when these two stream classes are coupled is developed in §9. The mean-field baseline Strict mean-field across streams: 𝐸MF(𝜋) = 𝐾 ∏ 𝑘=1 𝐸𝑘(𝜋𝑘), 𝐺MF(𝜋) = 𝐾 ∑ 𝑘=1 𝐺𝑘(𝜋𝑘), 𝑞MF(𝜋) = 𝐾 ∏ 𝑘=1 𝑞𝑘(𝜋𝑘), (3.4) with each 𝑞𝑘(𝜋𝑘) ∝𝐸𝑘(𝜋𝑘) exp(−𝛾𝑘𝐺𝑘(𝜋𝑘)) a single-stream posterior. This is the regime exemplified by pymdp’s factorized-A, factorized-B, factorized-policy treatment of multi-factor models [Heins et al., 2022]. Standing assumptions. - Every per-stream policy alphabet Π𝑘is finite; the joint Π = ∏𝑘Π𝑘is therefore finite. Continuous-policy extensions are conjectured in §20 (Q4) but are out of scope for the analytical core of this manuscript. - The per-stream priors 𝐸𝑘are strictly positive on Π𝑘(no exact zeros), so KL divergences and log-likelihoods are everywhere finite. - The per-stream EFE 𝐺𝑘and coupling potentials 𝐽, 𝐾𝑐are real-valued and bounded on Π, so 𝔼𝑞𝜆[ ⋅] exists for every observable used below and the Gibbs partition function 𝑍(𝜆) is real-analytic in 𝜆on [0, ∞). Standing notation. - 𝐻(⋅): Shannon entropy. - 𝐷KL(𝑝‖𝑞): Kullback-Leibler divergence. - 𝐼(𝑝) = ∑𝑘𝐻(𝑝𝑘)−𝐻(𝑝): total correlation (multi-information [McGill, 1954, Watanabe, 1960]) of joint 𝑝with respect to its 𝐾marginals 𝑝𝑘(see Eq. (5.3)). - ℳ: manifold of joint distributions on Π. - ℳMF ⊂ℳ: mean-field submanifold (product distributions); its e-flatness is recorded in Proposition 7.1 and developed in §7. Lambda Deformation: Definition and Properties In symbols: 𝑞𝜆(𝜋) ∝𝑞MF(𝜋) 𝑒𝜆(𝐽(𝜋)−𝛾𝐾𝑐(𝜋)), with 𝑞MF the mean-field baseline introduced in §3.3 and the entangled- prior / entangled-posterior expansion derived below. The symbols introduced below — 𝐽, 𝐾𝑐, 𝜆, 𝛾, ℰ𝜆, 𝑞𝜆— are cataloged in the unified notation glossary (§S6) with their LaTeX, Python, and Lean counterparts. Coupling potentials Introduce two real-valued coupling potentials on the joint policy space: 17 ## Page 19 • 𝐽∶Π →ℝ— habit coupling (prior-side): structural cross-stream tendencies that the agent has built up and considers a-priori plausible. • 𝐾𝑐∶Π →ℝ— preference coupling (EFE-side): cross-stream costs/preferences that show up in expected free energy beyond the per-stream EFEs. These need not be informed by anything outside the agent: they are parameters of the agent’s generative model, learned from experience. Definition: lambda-entangled policy posterior Define the 𝜆-entangled prior and 𝜆-entangled posterior as ℰ𝜆(𝜋) = 1 𝑍𝐸(𝜆) 𝐾 ∏ 𝑘=1 𝐸𝑘(𝜋𝑘) exp(𝜆𝐽(𝜋)) (4.1) 𝐺𝜆(𝜋) = 𝐾 ∑ 𝑘=1 𝐺𝑘(𝜋𝑘) + 𝜆𝐾𝑐(𝜋) (4.2) 𝑞𝜆(𝜋) ∝ℰ𝜆(𝜋) exp( −𝛾𝐺𝜆(𝜋)) = 1 𝑍(𝜆)[∏𝑘𝐸𝑘(𝜋𝑘)]exp(𝜆(𝐽(𝜋) −𝛾𝐾𝑐(𝜋)) −𝛾∑𝑘𝐺𝑘(𝜋𝑘)) (4.3) Boundary cases. - 𝜆= 0: ℰ0 = 𝐸MF, 𝐺0 = 𝐺MF, 𝑞0 = 𝑞MF. - 𝜆→∞: 𝑞𝜆collapses onto the modes of 𝐽−𝛾𝐾𝑐 — pure archetypal joint policies. (Here “modes” means elements of the argmax set argmax𝜋(𝐽(𝜋) −𝛾𝐾𝑐(𝜋)). As 𝜆→∞, 𝑞𝜆concentrates on this argmax set, with mass restricted to and re-normalized over those policies weighted by the bare-posterior measure 𝐸MF(𝜋) 𝑒−𝛾𝐺MF(𝜋); in particular, when 𝐸MF and 𝐺MF are constant on the argmax set, 𝑞𝜆concentrates uniformly on the set.) - Intermediate 𝜆: the regime of practical interest. For analytical separation of habit vs. preference coupling, one can carry two parameters 𝜆𝐸, 𝜆𝐺with coupling potentials 𝐽, 𝐾𝑐respectively. We use a single 𝜆in the body of the paper for clarity, with the two-parameter generalization appearing in §11 for comparative statics. The coupling parameter lambda as a precision-like coupling weight A central conceptual point: 𝜆is not merely an arbitrary engineering knob. In the exponential-family representation it behaves as a precision-like inverse-temperature on the coupling structure, dual (in the Legendre sense) to the sufficient statistics ⟨𝐽⟩and ⟨𝐾𝑐⟩under the joint posterior. This is mathematically analogous to the role 𝛾plays for EFE in the standard single-stream model, while remaining a distinct model parameter rather than a claim about any specific neural precision signal. Concretely: 𝜕log 𝑍(𝜆) 𝜕𝜆 = ⟨𝐽−𝛾𝐾𝑐⟩𝑞𝜆. (4.4) Updating 𝜆by gradient on free energy (§9) is therefore a formal analog of precision learning [Friston et al., 2014, Schwartenbeck et al., 2015, Limanowski et al., 2024]. We return to this in §9.4. Two consequences are worth flagging now. First, 𝜆can be learned from the same free-energy objective the agent already minimizes — there is no auxiliary regularizer, no separate meta-learner in the model. Second, under the model, coupling strength can vary with task context or learning history. Any biological, arousal, fatigue, or developmental reading is hypothesis-level until an empirical protocol estimates 𝜆from joint-action data; tonic over-coupling and under-coupling are therefore framed as hypotheses about joint-statistical signatures, not as diagnostic claims (§10). What J and K_c look like in practice Five archetypal forms span the modeling range, each tuned to a different kind of cross-stream dependency. The choice of 𝐽is therefore the substantive modeling decision — once 𝐽is fixed, the deformation in Eq. (5.2) is determined, and the framework’s theorems hold for any bounded-norm choice. The five archetypes: • Sparse pairwise. 𝐽(𝜋) = ∑(𝑖,𝑗)∈𝒞𝐽𝑖𝑗(𝜋𝑖, 𝜋𝑗) with 𝒞a small set of edges. Recovers pairwise Markov-random- field structure and is the natural generalization of factor graphs; appropriate when only a few stream pairs (e.g. left/right-hand pairs in motor coordination) carry meaningful joint dependence. 18 ## Page 20 • Tensor-network low-rank. 𝐽(𝜋) = log[MPS(𝜋1, … , 𝜋𝐾)] with bond dimension 𝑟. Recovers all the favorable algorithmic structure of matrix product states [Han et al., 2018]; bond dimension is a complexity dial that interpolates between mean-field (𝑟= 1) and arbitrary joint structure (full 𝑟). • Block-bidiagonal hierarchical. 𝐽couples only stream 𝑘to 𝑘+ 1. This is the structural analog used by the hierarchical / deep AIF witness-form mapping (§17.2): it captures cross-level coordination in the joint policy posterior, while temporal-scale separation and directed top-down / bottom-up message passing remain part of the source generative model. • Symbolic-task biased. 𝐽encodes a logical constraint (“if policy 1 is reach, then policy 2 is open hand”) via large-magnitude penalties on violating configurations. Appropriate when domain knowledge dictates discrete co-occurrences. • Learned tabular. 𝐽is a free parameter on Π (size ∏𝑘|Π𝑘|) and is learned end-to-end. Computationally infeasible for large 𝐾but conceptually clean and useful as the universal upper bound against which structured choices are benchmarked. The framework is agnostic to the choice of 𝐽, 𝐾𝑐— its theorems hold for any bounded-norm potentials. The art of the modeler is in choosing parsimonious, mechanistically interpretable forms. Entanglement Decomposition Theorem: Marginals, Coupling, and Total Correlation Statement The variational free energy under 𝑞𝜆admits a clean decomposition. Define 𝐹[𝑞𝜆] = 𝔼𝑞𝜆[𝛾𝐺𝜆(𝜋) −log ℰ𝜆(𝜋)] −𝐻(𝑞𝜆). (5.1) Let 𝑞𝑘 𝜆denote the marginal of 𝑞𝜆on stream 𝑘, and 𝐹[𝑞𝑘 𝜆] the marginal free energy if stream 𝑘were treated in isolation against its own 𝐸𝑘, 𝐺𝑘. Theorem 5.1 (Entanglement Decomposition). 𝐹[𝑞] = ∑ 𝑘 𝐹[𝑞𝑘] + 𝛾𝜆𝔼𝑞[𝐾𝑐] + log 𝑍𝐸(𝜆) −𝜆𝔼𝑞[𝐽] + 𝐼(𝑞) (5.2) where the total correlation 𝐼(𝑞) = ∑ 𝑘 𝐻(𝑞𝑘) −𝐻(𝑞) = 𝐷KL(𝑞‖ ∏ 𝑘 𝑞𝑘) (5.3) is non-negative and vanishes iff 𝑞𝜆is mean-field. (The sign on every term follows §S6.1 in S06 — specifically the plus-𝐼(𝑞𝜆) and the +𝛾𝜆⟨𝐾𝑐⟩conventions.) The Lean companion is a boundary statement auto-extracted from the live source: -- From `lean/ActinfPolicyEntanglement/Decomposition.lean:75` [status: **boundary**] /-- **Theorem 5.1 (Entanglement Decomposition)** — boundary witness form. Given a Mathlib-supplied algebraic split `F[q] = marginal_part + coupling_expectation + agentic_gain`, where `coupling_expectation` is the integrated `couplingLogWeight` against `q`, this theorem certifies the equation in the boundary fragment. Every coupling parameter `(J, K_c, γ, 𝜆)` is genuinely used via `couplingExpectationSkeleton`, so the statement is non-vacuous. **Typed-API-contract disclaimer.** The Lean body is literally `hWitness ↦hWitness` — the identity term on the algebraic split. This is **not** a stand-alone proof of Theorem 5.1; it is a typed-API contract that forces `(J, K_c, γ, 𝜆)` into the conclusion via `couplingExpectationSkeleton` and locks the four-term decomposition shape. The non-vacuous *algebraic* content of the decomposition (commutative-ring re-grouping of the four bookkeeping scalars) is discharged separately by `entanglement_decomposition_four_terms_assoc_skeleton` and `entanglement_decomposition_four_terms_commute_skeleton` below (genuine `CommScalar` proofs). The full *analytic* content (Gibbs expansion + KL chain rule) is supplied as `hWitness` and discharged 19 ## Page 21 by the separate MathlibProofs layer; the numerical realization is in `src/lean/decomposition.py` and verified at the dashboard invariant `decomposition_lhs_eq_rhs_max_residual` (worst-case `5.55e-16`). -/ theorem entanglement_decomposition {K Pol} (q : JointDist K Pol) (s : List (PolicySpace K Pol)) (logE G : PolicySpace K Pol →Float) (J K_c : CouplingPotential Float K Pol) (gamma lam : Float) (marginal_part agentic_gain : Float) (hWitness : variationalFreeEnergy q logE G gamma s = marginal_part + couplingExpectationSkeleton q s J K_c gamma lam + agentic_gain) : variationalFreeEnergy q logE G gamma s = marginal_part + couplingExpectationSkeleton q s J K_c gamma lam + agentic_gain := Honesty note. The Float boundary companion above carries status: boundary in manuscript/refs/labels.yaml, not status: proved: it type-checks under stock Lean v4.29.0 and locks the four- term algebraic skeleton, but its analytic content is supplied as a hypothesis. The analytic content itself is now machine-checked in ℝ: MathlibProofs.entanglement_decompo- sition_generalK proves, for general 𝐾and a general entangled 𝑞(positivity + normalization only; never assumed to factorize), the multi-information non-negativity, the KL chain-rule decomposition, and 𝑚-projection minimality — depending only on the three standard foundational axioms, with the previously-deferred product-marginalization core discharged from the standing positivity + normalization hypotheses without further structural assumptions, and negative-control-verified as non-vacuous. The full S01 boxed identity itself (F=Σ F[qᵏ]+γ𝜆⟨K_c⟩+log Z_E−𝜆⟨J⟩+I(q)) is then machine-checked in ℝby MathlibProofs.free_energy_decomposition_full for the genuine entangled posterior (log Z_E the definitional normalizer, foundational-only axioms, two independent negative controls). The Float companion is the numerically-corroborated computational image of the ℝproof; closing the Float↔ℝformal bridge is the one verification-stack interface residual (the open residual discussed at §21; interval brackets on the K=2 sweep grid in output/reports/float_real_residual.json corroborate Float decomposition residuals but do not discharge the bridge); the remaining typed-API rows are the analytic-discharge follow-on tracked at §20, not a separate verification gap). See the honest substantive / typed-API split in docs/reference/veridical_status.md for the round-by-round audit of which Lean theorems are substantive machine-checked proofs versus typed-API contracts. Proof sketch Expand 𝐹[𝑞𝜆] = 𝔼𝑞𝜆[𝛾𝐺𝜆−log ℰ𝜆] −𝐻(𝑞𝜆) using 𝛾𝐺𝜆(𝜋) = 𝛾∑ 𝑘 𝐺𝑘(𝜋𝑘) + 𝛾𝜆𝐾𝑐(𝜋), log ℰ𝜆(𝜋) = ∑ 𝑘 log 𝐸𝑘(𝜋𝑘) + 𝜆𝐽(𝜋) −log 𝑍𝐸(𝜆) (5.4) for the normalized entangled prior ℰ𝜆∝(∏𝑘𝐸𝑘) 𝑒𝜆𝐽. Linearity of expectation separates 𝔼[𝛾𝐺𝜆] and 𝔼[log ℰ𝜆] into per-stream pieces plus the 𝛾𝜆⟨𝐾𝑐⟩, 𝜆⟨𝐽⟩, and log 𝑍𝐸(𝜆) terms. The entropies −𝐻(𝑞𝜆) combine with ∑𝑘𝔼𝑞𝑘 𝜆[𝛾𝐺𝑘−log 𝐸𝑘] into ∑𝑘𝐹[𝑞𝑘 𝜆] + ( ∑𝑘𝐻(𝑞𝑘 𝜆) −𝐻(𝑞𝜆)); the parenthesis is multi-information 𝐼(𝑞) = ∑ 𝑘 𝐻(𝑞𝑘) −𝐻(𝑞) = 𝐷KL(𝑞‖ ∏ 𝑘 𝑞𝑘) (5.3) , i.e. 𝐼(𝑞𝜆). Altogether this yields 𝐹[𝑞] = ∑ 𝑘 𝐹[𝑞𝑘] + 𝛾𝜆𝔼𝑞[𝐾𝑐] + log 𝑍𝐸(𝜆) −𝜆𝔼𝑞[𝐽] + 𝐼(𝑞) (5.2) . Full line-by-line algebra is in §A; the Python record entanglement_decomposition_rhs sums the same four grouped terms and matches the Gibbs definition of 𝐹on random joints (see tests/test_decomposition.py). What the decomposition says Three terms, three readings: (i) ∑𝑘𝐹[𝑞𝑘 𝜆]. The free energy that would obtain if each stream were optimized in isolation against the marginal of 𝑞𝜆. This is not the same as ∑𝑘𝐹[𝑞MF 𝑘 ], because the marginals 𝑞𝑘 𝜆are themselves shaped by coupling — coupling deforms what a stream considers a-posteriori plausible even before we charge the multi-information cost. 20 ## Page 22 (ii) 𝜆(𝛾⟨𝐾𝑐⟩−⟨𝐽⟩). The coupling cost — what it costs (or pays) the agent to maintain the joint structure encoded by the potentials. Sign depends on alignment between habit coupling 𝐽(which the agent likes) and preference-side coupling 𝐾𝑐(which contributes EFE). When 𝐽and 𝐾𝑐point in compatible directions — e.g., when habitual joint policies happen to also minimize joint EFE — this term can be net negative and pays for itself. (iii) 𝐼(𝑞𝜆) ≥0. The multi-information term appears with a plus sign in 𝐹[𝑞] = ∑ 𝑘 𝐹[𝑞𝑘] + 𝛾𝜆𝔼𝑞[𝐾𝑐] + log 𝑍𝐸(𝜆) −𝜆𝔼𝑞[𝐽] + 𝐼(𝑞) (5.2) : holding the marginals fixed, any genuine cross-stream correlation raises the Gibbs variational objective by exactly 𝐼(𝑞𝜆) nats. When joint structure still pays off for the agent is a comparison with the coupling / EFE / log-partition bundle in the same identity — not literal subtraction of 𝐼from “free energy” in isolation. Corollary 5.2–Corollary 5.4 formalize the sign bookkeeping of that trade-off. Read together, the three terms expose the central trade-off of policy entanglement. The marginal sum (i) tracks how each stream is faring on its own slice of the deformed posterior; the coupling bundle (ii) is the price tag of maintaining the structure encoded in 𝐽and 𝐾𝑐, and can be paid in either direction depending on whether habit and preference are aligned or in tension; the multi-information (iii) is the correlation surcharge that any non-mean-field joint owes purely for being correlated. Coupling pays for itself precisely when the bundle (ii) is sufficiently negative to absorb both the correlation surcharge (iii) and any worsening of per-stream marginals (i). Stating it this way also clarifies why the framework refuses to call (iii) a “cost” in isolation: 𝐼(𝑞𝜆) is the price of joint structure measured against mean-field, but (i) and (ii) measure how much that structure buys back, and only the sum across all three is a meaningful free-energy comparison. The Lean companions for the three immediate corollaries are auto-extracted below. Corollary 5.2 (the coupling-pays-for-itself verdict) is a tri-state classifier from the sign of the bookkeeping, now upgraded to a proved theorem (status: proved) whose Lean form discharges the sign-soundness identity by direct case analysis on the bookkeeping variable: -- From `lean/ActinfPolicyEntanglement/Decomposition.lean:168` [status: **proved**] /-- **Corollary 5.2 correctness theorem (boundary identity)**: the `couplingVerdict` Boolean is `true` precisely when the coupling tax is strictly less than the agentic gain — i.e. the verdict semantics faithfully decide the "coupling-pays-for-itself" predicate. This pins the verdict's contract on the boundary fragment: a `true` answer is *not* an oracle assertion but a Lean-level proof that `tax < gain`. Discharged by unfolding the `decide` and forwarding the proof component, no `sorry`. -/ theorem couplingVerdict_correct (gain tax : Float) : couplingVerdict gain tax = true ↔tax < gain := by Corollary 5.3 (mean-field reduction at 𝜆= 0) collapses the four-summand bookkeeping to its sum-of-marginals + total- correlation-gain pair: -- From `lean/ActinfPolicyEntanglement/Decomposition.lean:195` [status: **proved**] /-- **Corollary 5.3 (Mean-field optimum at 𝜆= 0)**: at `𝜆= 0`, the coupling log-weight contribution vanishes pointwise. Polymorphic over `[CommScalar α]`; combine with `entanglement_decomposition` to recover the pure mean-field statement `F[q_0] = Σ_k F[q_0^k] + agentic_gain`. -/ theorem couplingLogWeight_pointwise_at_zero {α : Type} [CommScalar α] {K Pol} (J K_c : CouplingPotential α K Pol) (gamma : α) (π : PolicySpace K Pol) : couplingLogWeight J K_c gamma 0 π = 0 := Corollary 5.4 (strict gain when 𝑞is non-mean-field) is the sign companion of Eq. (5.3). Unlike the two proved corollaries above, its Lean companion is a typed boundary witness (status: boundary, faithfulness: typed-witness): the strict-gain inequality is carried as a typed contract, with the analytic discharge at the Mathlib layer. -- From `lean/ActinfPolicyEntanglement/Decomposition.lean:215` [status: **boundary**] /-- **Corollary 5.4 (Total-correlation unfolding)**: the boundary fragment's `totalCorrelation` is by construction the per-stream entropy sum minus the joint entropy. This forwarder makes the definitional unfolding available to downstream modules without re-importing `FreeEnergy`'s namespace. The strict-positivity claim `I(q) > 0 iff q is not mean-field` is the `Iq > 0 ↔¬ IsMeanField q` companion that requires Mathlib's KL-non-negativity (see `IsNonNegMultiInformation` in [`FreeEnergy.lean`](FreeEnergy.lean)) and is exposed by the `MathlibProofs` extension. Stock-Lean, zero-`sorry`. -/ theorem totalCorrelation_def_unfold {K Pol} 21 ## Page 23 (q : JointDist K Pol) (s : List (PolicySpace K Pol)) (sumStreamEntropies : Float) : totalCorrelation q s sumStreamEntropies = sumStreamEntropies - shannonEntropy q s := rfl Optimal coupling: existence of lambda* Theorem 5.5 (Existence of optimal coupling). For fixed 𝐽, 𝐾𝑐with bounded potentials, 𝐹[𝑞𝜆] is real-analytic in 𝜆on [0, ∞) and admits the closed exponential-family identity 𝐹[𝑞𝜆] = log 𝑍𝐸(𝜆) −log 𝑍(𝜆) (5.8) The Lean boundary companion threads the algebraic identity through the coupling-log-weight skeleton so every parameter (𝐽, 𝐾𝑐, 𝛾, 𝜆) is genuinely referenced: -- From `lean/ActinfPolicyEntanglement/Decomposition.lean:243` [status: **boundary**] /-! ## Theorem 5.5 — closed exponential-family form of `F[q_𝜆]` The Gibbs decomposition `F[q] = Σ F[q^k] + γ𝜆⟨K_c⟩+ log Z_E(𝜆) - 𝜆⟨J⟩+ I(q)` collapses to the strikingly clean identity ``` F[q_𝜆] = log Z_E(𝜆) - log Z(𝜆), ``` where `log Z_E(𝜆)` is the entangled-prior log-partition and `log Z(𝜆)` is the entangled-posterior log-partition. See [`manuscript/04_entanglement_decomposition.md`](../../manuscript/04_entanglement_decomposition.md) ([Theorem 5.5](../../manuscript/refs/labels.yaml#thm_4_2)) and the proof appendix [`manuscript/S01_proof_of_decomposition_theorem.md`](../../manuscript/S01_proof_of_decomposition_theorem.md). The boundary fragment exposes the identity as a *witness-consuming* statement: the caller (the separate additive `MathlibProofs` layer or the numerical Python layer) supplies the algebraic equality `vfe = logZE - logZ`, and the boundary fragment threads `(𝜆, J, γ, K_c)` through `couplingExpectationSkeleton` so every parameter is genuinely referenced and the statement is non-vacuous. Polymorphic over `[CommScalar α]`. -/ theorem freeEnergy_closedForm_witness {α : Type} [CommScalar α] {K Pol} (vfe logZE logZ : α) (_s : List (PolicySpace K Pol)) (J K_c : CouplingPotential α K Pol) (gamma lam : α) (hWitness : vfe = logZE - logZ) : vfe = logZE - logZ ∧(∀π : PolicySpace K Pol, couplingLogWeight J K_c gamma lam π = lam * J π - gamma * lam * K_c π) := by where 𝑍(𝜆) = ∑𝜋𝐸MF(𝜋) 𝑒𝜆(𝐽−𝛾𝐾𝑐)(𝜋)−𝛾𝐺MF(𝜋) is the normalizer of 𝑞𝜆and 𝑍𝐸(𝜆) = ∑𝜋𝐸MF(𝜋) 𝑒𝜆𝐽(𝜋) is the normalizer of the entangled prior. Differentiating once gives d𝐹[𝑞𝜆] d𝜆 = ⟨𝐽⟩ℰ𝜆−⟨𝐽⟩𝑞𝜆+ 𝛾⟨𝐾𝑐⟩𝑞𝜆 (5.9) so 𝜆↦𝐹[𝑞𝜆] has at least one stationary point in (0, ∞) whenever the marginal slope is negative, ⟨𝐽⟩𝑞0 −𝛾⟨𝐾𝑐⟩𝑞0 > ⟨𝐽⟩𝐸MF, (5.10) i.e. when the posterior coupling alignment net of EFE cost exceeds the prior coupling alignment. Since 𝐹is real- analytic and bounded below on [0, ∞) — boundedness follows from the compactness of the simplex on a finite Π and the boundedness of the potentials 𝐽, 𝐾𝑐, 𝐺𝑘standing-assumed in §3.3, so log 𝑍𝐸(𝜆) and log 𝑍(𝜆) are continuous bounded functions of 𝜆— and 𝐹′(0) < 0 under the stated marginal-slope condition, 𝐹′(𝜆) achieves a zero in some open interval and a stationary point 𝜆⋆∈(0, ∞) exists. Since the multi-information 𝐼attains its minimum at the mean-field surface, d𝐼/d𝜆|0 = 0 identically. To see this in one line: by the chain rule along the e-geodesic, the covariance form is d𝐼(𝑞𝜆) d𝜆 = Cov𝑞𝜆(𝐽−𝛾𝐾𝑐, log 𝑞𝜆−log ̂𝑚(𝑞𝜆)) (5.11) 22 ## Page 24 A derivation along the e-geodesic from the closed identity Eq. (7.3) is in §9; at 𝜆= 0, 𝑞0 = 𝑞MF = ̂𝑚(𝑞0) pointwise (here ̂𝑚(𝑞) = ∏𝑘𝑞𝑘is the m-projection of 𝑞onto the mean-field submanifold ℳMF, defined in §7.1), so log 𝑞0 −log ̂𝑚(𝑞0) ≡0 on Π and the covariance vanishes. The Fisher contribution to 𝐹therefore lives at second order (Eq. (A.15) and Proposition 11.1; see also §B). Under the symmetric standing prior 𝐸MF = Unif with ⟨𝐽⟩𝐸MF = 0, the first-order condition collapses to the simpler form ⟨𝐽⟩𝑞0 > 𝛾⟨𝐾𝑐⟩𝑞0 used throughout §6 and §11. Theorem 5.6 (Convexity of 𝐹in 𝜆— witness-form). If 𝐽−𝛾𝐾𝑐is log-concave on Π (in the finite-simplex sense developed in §B), then 𝜆↦𝐹[𝑞𝜆] is convex on [0, ∞) and 𝜆∗is unique. The boundary fragment ships the witness-consuming Lean companion Convexity.freeEnergy_convex_in_lam_witness; the analytic content is a structural witness that Mathlib4 can discharge from convex-analysis and log-partition facts without changing the boundary theorem. Theorem 5.6 says, in cognitive terms: when habit coupling and preference coupling are coherent (no internal contradictions in what joint policies the agent prefers and habituates), the optimal entanglement strength is uniquely determined. When they are incoherent, the framework predicts multiple stable coupling regimes — a point we develop into a phase-structure analysis in §10. Takeaways 1. The decomposition is exact, not an approximation. Variational free energy under the entangled posterior is identically the sum of per-stream marginal free energies, a coupling/partition bundle, and a non-negative multi-information term — see Eq. (5.2). 2. Coupling pays for itself iff the surplus exceeds the multi-information cost. The optimum 𝜆⋆is determined by a single first-order condition balancing ⟨𝐽−𝛾𝐾𝑐⟩against the total-correlation slope. 3. Coherent potentials yield a unique optimum; incoherent potentials predict phase regimes. Convexity of 𝐹in 𝜆(Theorem 5.6) is the theoretical hinge: when it holds, 𝜆⋆is uniquely determined; when it fails, multiple stable couplings co-exist (see §10). Worked Examples: Bernoulli Toy, Motor-Attention Coupling, and Multi-Timescale Coupling The K=2 Bernoulli toy: full closed form In the symmetric 𝐾= 2 Bernoulli toy (defined just below) the closed-form multi-information has the body-scaling identity 𝐼(𝜆) = 𝜆𝐽0 tanh(𝜆𝐽0) −log cosh(𝜆𝐽0) = log 2 −𝐻𝑏(𝜎(2𝜆𝐽0)), (6.1) where 𝐻𝑏is binary entropy and 𝜎is the logistic; the appendix-scaling form (𝐽∈{± 1 2}) is derived line-by-line in §C. Not 𝐼(𝜆) = log cosh 𝜆, which would be an algebra error. Two streams, each with two policies: Π1 = Π2 = {0, 1}. Marginal priors 𝐸𝑘= Unif. Marginal EFEs 𝐺𝑘(0) = 𝐺𝑘(1) = 0 (so the streams are EFE-degenerate; all action is in the coupling). Bilinear coupling 𝐽(𝜋1, 𝜋2) = 𝐽0 (2𝜋1 −1)(2𝜋2 −1) — i.e., 𝐽= +𝐽0 on aligned, 𝐽= −𝐽0 on anti-aligned. Set 𝛾𝐾𝑐= 0 for clarity. The joint posterior is 𝑞𝜆(𝜋1, 𝜋2) = 𝐸MF(𝜋) 𝑒𝜆𝐽(𝜋) 𝑍(𝜆) = 𝑒𝜆𝐽0 (2𝜋1−1)(2𝜋2−1) 4 cosh(𝜆𝐽0) , (6.2) with the normalized-joint partition (using the normalized mean-field prior 𝐸MF(𝜋) = 1/4 on each of the four atoms) 𝑍(𝜆) = ∑ 𝜋 𝐸MF(𝜋) 𝑒𝜆𝐽(𝜋) = 1 4(2𝑒𝜆𝐽0 + 2𝑒−𝜆𝐽0) = cosh(𝜆𝐽0). (6.3) (The factor 1/4 comes from 𝐸MF; the unnormalized atom-sum 2𝑒𝜆𝐽0 + 2𝑒−𝜆𝐽0 = 4 cosh(𝜆𝐽0) is four times 𝑍(𝜆).) So 𝑞𝜆(𝜋) = 𝐸MF(𝜋) 𝑒𝜆𝐽(𝜋)/𝑍(𝜆) = 𝑒𝜆𝐽(𝜋)/(4 cosh(𝜆𝐽0)), as displayed above. Marginals: 𝑞1 𝜆(𝜋1) = 𝑞2 𝜆(𝜋2) = 1/2 (symmetry, so 𝐻(𝑞𝑘 𝜆) = log 2). For the joint, the four atoms have masses 𝜎(2𝜆𝐽0)/2 on the two aligned configurations and (1 −𝜎(2𝜆𝐽0))/2 on the two anti-aligned, where 𝜎(𝑥) = 1/(1 + 𝑒−𝑥) 23 ## Page 25 is the logistic. Direct computation gives the joint entropy 𝐻(𝑞𝜆) = log 2 + 𝐻𝑏(𝜎(2𝜆𝐽0)) with binary entropy 𝐻𝑏(𝑝) = −𝑝log 𝑝−(1 −𝑝) log(1 −𝑝). The total correlation is then 𝐼(𝑞𝜆) = ∑ 𝑘 𝐻(𝑞𝑘 𝜆) −𝐻(𝑞𝜆) = 2 log 2 −log 2 −𝐻𝑏(𝜎(2𝜆𝐽0)) = log 2 −𝐻𝑏(𝜎(2𝜆𝐽0)). (6.4) Equivalently, in tanh form (the algebraic identity log 2 −𝐻𝑏(𝜎(𝑥)) = 𝑥 2 tanh(𝑥/2) −log cosh(𝑥/2)): 𝐼(𝑞𝜆) = 𝜆𝐽0 tanh(𝜆𝐽0) −log cosh(𝜆𝐽0) = log 2 −𝐻𝑏(𝜎(2𝜆𝐽0)) , 𝜎(𝑥) = 1 1 + 𝑒−𝑥 (6.5) This is the well-known mutual information of an Ising pair at inverse temperature 𝜆𝐽0. See §C for the line-by-line derivation; the body uses the bilinear scaling 𝐽= 𝐽0(2𝜋1 −1)(2𝜋2 −1) while the appendix uses the swing- 1 2 form 𝐽∈{± 1 2}, related by 𝜆body ⋅𝐽0 = 𝜆app/2. The free energy decomposition 𝐹[𝑞] = ∑ 𝑘 𝐹[𝑞𝑘] + 𝛾𝜆𝔼𝑞[𝐾𝑐] + log 𝑍𝐸(𝜆) −𝜆𝔼𝑞[𝐽] + 𝐼(𝑞) (5.2) , applied with 𝐾𝑐= 0 and both marginal free energies 𝐹[𝑞𝑘 𝜆] = 0 (symmetric priors, zero per-stream EFE), gives: 𝐹[𝑞𝜆] = log cosh(𝜆𝐽0) −𝜆𝐽0 tanh(𝜆𝐽0) + 𝐼(𝑞𝜆) = 0, (6.7) since log 𝑍𝐸(𝜆) = log cosh(𝜆𝐽0), 𝜆⟨𝐽⟩𝑞𝜆= 𝜆𝐽0 tanh(𝜆𝐽0), and 𝐼(𝑞𝜆) = 𝜆𝐽0 tanh(𝜆𝐽0) −log cosh(𝜆𝐽0) — these three terms cancel identically. The result 𝐹[𝑞𝜆] ≡0 is expected: when 𝐺𝑘= 𝐾𝑐= 0 the posterior equals the prior (𝑞𝜆= ℰ𝜆) and the Gibbs variational objective is zero by construction. Optimal 𝜆∗: Because 𝐹[𝑞𝜆] = 0 for all 𝜆, the VFE landscape is flat — there is no free-energy gradient to set 𝜆. This is the degenerate Ising limit, and it resolves the moment 𝐺𝑘≠0 or 𝐾𝑐≠0, whereupon a well-defined finite 𝜆⋆ appears (see §6.2). The toy is genuinely instructive: it isolates the pure role of the habit potential 𝐽. Without a preference coupling 𝐾𝑐, free energy places no penalty on entanglement — all coupling levels are equally consistent with the model. The role of 𝐾𝑐is to create the free-energy gradient that controls 𝜆⋆; this is the formal version of “habits are cheap; planning to satisfy preferences is expensive.” The closed-form mutual-information curve Eq. (6.5), the empirical numerical realization, and the joint posterior at a representative 𝜆= 2 are reproduced numerically by scripts/parameter_sweep.py and visualized below; agreement with the closed form is to floating tolerance (≤1𝑒−06 over 121 grid points spanning 𝜆∈[0, 6], see output/data/parameter_sweep.csv). Sentinel values: 𝐼(𝜆= 1) = 0.1109 nats, 𝐼(𝜆= 2) = 0.3278 nats. Two-stream motor + attention with realistic EFE Stream 1 = motor (reach left vs. reach right). Stream 2 = attention (look left vs. look right). Per-stream EFEs: 𝐺1 depends on a hidden target location; 𝐺2 depends on epistemic value of foveation. Habit coupling 𝐽= strong positive on aligned (look-where-you-reach) and slightly negative on anti-aligned. 𝐾𝑐= mild positive penalty on simultaneous-novel-action (“don’t change two things at once”). This recovers a familiar pattern: optimal 𝜆∗is finite and positive; the agent learns to align gaze and reach habitually, but the EFE cost of doubling novelty prevents over-rigidity. Empirically (see scripts/manuscript_- variables.py::_motor_attention_facts), the joint probability of an aligned (look-where-you-reach) outcome grows from 𝑃align(𝜆= 0) = 0.5242 to 𝑃align(𝜆= 1) = 0.8451 to 𝑃align(𝜆= 2) = 0.9643. The empirical suite in §13 already sweeps 𝜆and renders the relevant observables rather than leaving them as a schematic: total correlation, Schmidt entropy (§8), free-energy surfaces, aligned-policy mass, and tensor-train rank profiles. In the two-stream worked example, the show-not-tell pattern is visible in Fig. 1, Fig. 8, and Fig. 2: total correlation grows and saturates, Schmidt entropy rises away from the mean-field boundary and then bends toward the archetypal regime, and the free-energy surface identifies the coupling range where the utility surplus pays for the information cost. The closed-form alignment-inversion map 𝜆⋆(Δalign) for the symmetric K=2 toy — i.e. the coupling that realizes a given target alignment Δalign = 𝛼(𝜆) = tanh(𝜆/2) — is 𝜆⋆(Δalign) = 2 arctanh(Δalign Δmax ) (6.8) 24 ## Page 26 Figure 1: The K=2 Ising joint at 𝜆= 2 concentrates probability on the two aligned policies (diagonal) while the per-stream marginals (side bars) remain symmetric. The inset residual 𝑞−∏𝑘𝑞𝑘is non-zero — the visual signature of departure from the mean-field manifold, and the m-projection witness of Proposition 7.2 (marginalization = m-projection minimizes KL). Joint built via lean.bernoulli_toy.ising_joint_posterior at 𝜆= 2 (JOINT_HEATMAP_LAMBDA); panel layout from visualizations.joint_plots.plot_joint_heatmap_with_marginals. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 25 ## Page 27 Figure 2: The closed-form mutual information agrees with the empirical sampler to sweep tolerance (≤1𝑒−06 across 121 grid points). The curve 𝐼(𝜆) = log 2−𝐻𝑏(𝜎(𝜆)) grows from 0 at 𝜆= 0 (independence) and satu- rates at log 2 ≈0.693 as |𝜆| →∞(perfect alignment). Closed form (lean.bernoulli_toy.ising_mutual_information, Eq. (6.5)) and empirical (lean.bernoulli_toy.empirical_mutual_information) are overlaid on the 121-point sweep from simulation.hyperparameters.PARAMETER_SWEEP_LAMBDAS (𝜆∈[0, 6]); CSV at output/data/parameter_sweep.csv. This is the K=2 specialization of the decomposition theorem Theorem 5.1 (Lean companion ActinfPolicyEntan- glement.Decomposition.entanglement_decomposition). Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 26 ## Page 28 (see Eq. (6.8); this is target-alignment inversion, not the free-energy first-order condition, which is treated as a separate VFE-optimization problem in §C and reduces to 𝜆⋆= 2𝑢in the small-utility limit). The saturating monotone shape is recovered numerically by src/lean/bernoulli_toy.py::optimal_lambda. Numerical anchors: 𝜆⋆(0.5) = 1.0986, 𝜆⋆(0.9) = 2.9444. Figure 3: The coupling that realizes a target alignment Δalign in the K=2 Bernoulli toy is 𝜆⋆(Δalign) = 2 arctanh(Δalign/Δmax). This is the alignment-inversion formula — the inverse of the alignment–coupling correspondence 𝛼(𝜆) = tanh(𝜆/2) — not a VFE optimum. The actual VFE-optimal coupling under a utility scalar 𝑢in the same toy is 𝜆⋆= 2𝑢at small 𝑢and only coincides with 2 arctanh(𝑢) in that limit (see §C). Numerical witnesses for the existence (Theorem 5.5) and uniqueness via convexity (Theorem 5.6) of the VFE-optimal 𝜆⋆are separate from this alignment-inversion curve. Closed form from lean.bernoulli_toy.optimal_lambda evaluated on the 191-point sweep Δalign/Δmax ∈[−0.95, 0.95] (simulation.hyperparameters.OPTIMAL_LAMBDA_DELTAS). Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. Multi-timescale coupling One stream can be read as fast attentional control and another as a slower navigational plan. A sparse hierarchical 𝐽that couples the fast policy to the first decision point of the slower policy illustrates the coupling shadow of hierarchical AIF [Pezzulo et al., 2018]: the posterior records cross-level compatibility without claiming to reproduce the full directed message-passing schedule or temporal-scale separation of the source process theory. §17.2 states the corresponding witness-form concentration claim and its limitations. Information Geometry: Geodesics, Flatness, and Pythagorean Decom- position Dual coordinates and the mean-field submanifold Equip the simplex of joint distributions on Π with the standard dually-flat structure [Amari, 1985, Amari and Nagaoka, 2000, Amari, 2016]: • e-affine (exponential) coordinates: natural parameters 𝜃of an exponential family. 27 ## Page 29 Figure 4: Coupling pays off only when the utility surplus is large enough to overcome the multi- information cost. The free-energy curve 𝐹[𝑞𝜆] collapses to a flat zero at zero utility (no preference signal ⇒ no incentive to leave the mean-field manifold) and becomes monotonically decreasing as the surplus Δutil grows. Four utility levels Δutil ∈{0, 0.5, 1, 2} shown. All four curves are convex in 𝜆on [0, ∞) — the numerical witness of Theorem 5.6 (convexity of 𝐹in 𝜆). Computed via lean.bernoulli_toy.ising_free_energy_curve on the 121- point sweep PARAMETER_SWEEP_LAMBDAS. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 28 ## Page 30 • m-affine (mixture) coordinates: expectation parameters 𝜂= ∇𝜓(𝜃) where 𝜓is the log-partition. • Riemannian metric: Fisher information. • Canonical divergence: 𝐷KL. The mean-field submanifold ℳMF ⊂ℳis the set of product distributions on Π. Standard facts: Proposition 7.1. ℳMF is e-flat in ℳ: closed under exponential geodesics (interpolations affine in log- probability). The Lean companion Geometry.mfImage_isMeanField machine-checks only the definitional membership IsMeanField(mfToJoint 𝑚) (every product distribution is mean-field, by rfl); it does not discharge the e-flatness / closure-under-log-mixtures identity, which is the open real-analytic content scoped to the separate Mathlib layer (registry status: proved but faithfulness: statement-restricted — see docs/reference/veridical_status.md). Proposition 7.2 (m-projection / marginalization). For any 𝑞∈ℳ, the m-projection onto ℳMF is given by taking marginals: ̂𝑚(𝑞) = ∏ 𝑘 𝑞𝑘= arg min 𝑝∈ℳMF 𝐷KL(𝑞‖ 𝑝). (7.1) Proposition 7.3 (Total correlation as Bregman divergence to projection). 𝐼(𝑞) = 𝐷KL(𝑞‖ ̂𝑚(𝑞)). (7.2) Hence the multi-information appearing in Theorem 5.1 is precisely the Bregman divergence from the joint posterior to its mean-field projection — the geometric “departure” from the mean-field surface. Two corollaries follow immediately and are useful intuition pumps for the rest of the manuscript: • Non-negativity. 𝐼(𝑞) ≥0 with equality iff 𝑞is mean-field, recovering the entropy sub-additivity inequality 𝐻(𝑞) ≤∑𝑘𝐻(𝑞𝑘) as the expanded form of Eq. (5.3). • Pythagorean intuition. Because ̂𝑚(𝑞) is the m-projection of 𝑞onto ℳMF, 𝐼(𝑞) is the closest-point KL distance from 𝑞to the mean-field surface; everything farther on ℳMF is recovered by the Pythagorean decomposition Eq. (7.4) below. The Lean companions for these three propositions are auto-extracted from the live source under lean/ActinfPolicyEntanglement/Geometry.lean and lean/ActinfPolicyEntanglement/FreeEnergy.lean: -- From `lean/ActinfPolicyEntanglement/Geometry.lean:40` [status: **proved**] /-- **`mfImage_isMeanField`** (registry `prop_6_1`, Prop 7.1, `faithfulness: statement-restricted`). This theorem proves only that the product distribution induced by mean-field marginals *is* mean-field — definitional membership `IsMeanField (mfToJoint m)`, discharged by `rfl`. It does **NOT** prove the named manuscript proposition "the MF submanifold is e-flat" (closure under exponential geodesics / affine-in-θ); that real-analytic content is the open target scoped to the separate Mathlib layer (cf. `entangledFamily_eGeodesic` for the affine-in-𝜆identity). The name was deliberately changed from the prior `mfSubmanifold_eFlat` so the declaration's name states what it actually proves. -/ theorem mfImage_isMeanField {K Pol} (m : MFDist K Pol) : IsMeanField (mfToJoint m) := by -- From `lean/ActinfPolicyEntanglement/Geometry.lean:77` [status: **proved**] /-- **`mProjection_kl_eq_self_when_meanfield`** (registry `prop_6_2`, Prop 7.2, `faithfulness: statement-restricted`). This theorem proves only the conditional equality `KL(q ‖ mfToJoint m) = KL(q ‖ q)` *under the hypothesis* `h : q = mfToJoint m` (i.e. `q` is already mean-field). It does **NOT** prove the named manuscript proposition that the m-projection *minimises* KL — the information-projection optimality `∀p ∈M_MF, D_KL(q‖m̂(q)) ≤D_KL(q‖p)` is the open analytic target for the separate Mathlib layer. The name was deliberately changed from the prior `mProjection_minimises_kl` so the declaration's name states what it actually proves (an equality when `q` is already the projection, not a minimality result). -/ theorem mProjection_kl_eq_self_when_meanfield {K Pol} (q : JointDist K Pol) (m : MFDist K Pol) (h : ∀π, q π = mfToJoint m π) (s : List (PolicySpace K Pol)) : kl q (mfToJoint m) s = kl q q s := by -- From `lean/ActinfPolicyEntanglement/FreeEnergy.lean:140` [status: **witness**] /-- **Proposition 7.3 (boundary witness form)**: given the per-stream entropy sum and the value of `KL(q ‖ m̂(q))` together with the algebraic identity binding them, the boundary fragment certifies the total correlation equals the KL to the m-projection. Stock-Lean, zero-`sorry`. 29 ## Page 31 **Typed-API-contract disclaimer.** Not a stand-alone proof of the KL-chain-rule identity `I(q) = KL(q ‖ ∏_k q^k)`; a typed-API contract. The caller supplies `hWitness : sumStreamEntropies −shannonEntropy q s = klToMProj`; the boundary fragment unfolds `totalCorrelation` and forwards. -/ theorem totalCorrelation_eq_kl_to_mprojection {K Pol} (q : JointDist K Pol) (s : List (PolicySpace K Pol)) (sumStreamEntropies klToMProj : Float) (hWitness : sumStreamEntropies - shannonEntropy q s = klToMProj) : totalCorrelation q s sumStreamEntropies = klToMProj := by The lambda-family is an e-geodesic Theorem 7.4. The family {𝑞𝜆}𝜆∈ℝis an e-geodesic in ℳ: log 𝑞𝜆(𝜋) is affine in 𝜆up to the normalizing constant. The geodesic departs ℳMF at 𝜆= 0 in the direction defined by 𝐽−𝛾𝐾𝑐. Proof. Expand log 𝑞𝜆(𝜋) using the definition of the 𝜆-entangled prior ℰ𝜆and the Gibbs form §4.2: the only 𝜆- dependent terms are 𝜆𝐽(𝜋) and the normalizer log 𝑍(𝜆). Subtracting log 𝑍(𝜆) — which is independent of 𝜋— leaves the e-geodesic identity log 𝑞𝜆(𝜋) + log 𝑍(𝜆) = ∑ 𝑘 log 𝐸𝑘(𝜋𝑘) −𝛾∑ 𝑘 𝐺𝑘(𝜋𝑘) + 𝜆(𝐽(𝜋) −𝛾𝐾𝑐(𝜋)) (7.3) so 𝜋↦log 𝑞𝜆(𝜋) + log 𝑍(𝜆) is affine in 𝜆at every fixed 𝜋with slope 𝐽(𝜋) −𝛾𝐾𝑐(𝜋). ■ The Lean companion (proved by forwarding to the linearity lemma in Coupling.lean): -- From `lean/ActinfPolicyEntanglement/Geometry.lean:95` [status: **forwarder**] /-- **Theorem 7.4** (forwarder). Polymorphic over `[CommScalar α]`. -/ theorem entangledFamily_eGeodesic {α : Type} [CommScalar α] {K Pol} (J K_c : CouplingPotential α K Pol) (gamma lam1 lam2 : α) (π : PolicySpace K Pol) : couplingLogWeight J K_c gamma lam1 π - couplingLogWeight J K_c gamma lam2 π = (lam1 - lam2) * (J π - gamma * K_c π) := The affineness is straightforwardly observable numerically (see Eq. (7.3)): at every 𝜋the unnormalized log-weight traces a straight line in 𝜆with slope 𝐽(𝜋) −𝛾𝐾𝑐(𝜋). The same geodesic is also visible in a low-dimensional summary plane (Fig. 45): projecting the K=2 Ising joint onto its aligned-corner mass and off-diagonal disparity traces a curve that departs the mean-field anchor at 𝜆= 0 and bends monotonically toward an archetypal corner. This places the framework in an exceptionally well-developed geometric setting. Concretely: • Revertibility = m-projection. To revert an entangled posterior to mean-field, marginalize. This is an analytic, differentiable operation. The framework therefore predicts that marginal behavioral statistics are recoverable from coupled policies by the same projection used in the model; factor-isolation experiments are the right empirical design for testing that recovery rather than evidence that the biological system explicitly performs this operation. • Manifold envelope. The “envelope” of joint distributions reachable with bounded coupling-potential norm is a tubular neighborhood of ℳMF in the Fisher metric, of radius proportional to 𝜆⋅‖𝐽−𝛾𝐾𝑐‖. • Proposition 7.5 (Pythagorean decomposition). For any joint 𝑞and any reference mean-field distribution 𝑞∗ 0, the dually-flat Pythagorean theorem gives 𝐷KL(𝑞‖ 𝑞∗ 0) = 𝐼(𝑞) + 𝐷KL( ̂𝑚(𝑞) ‖ 𝑞∗ 0) (7.4) so 𝐷KL(𝑞‖ 𝑞∗ 0) splits orthogonally into the “departure from MF” term 𝐼(𝑞) and the “MF-to-MF distance” term 𝐷KL( ̂𝑚(𝑞) ‖ 𝑞∗ 0) — see also Eq. (7.4). The Lean companion for Proposition 7.5 is a witness-consuming boundary form: the caller supplies the dual-flat Pythagorean decomposition as a structural witness (dualFlat_pythagorean_witness). The current manuscript claims that typed contract plus the numerical revertibility witness; the Mathlib4 discharge target is the finite-KL chain rule and Bregman-divergence identity. -- From `lean/ActinfPolicyEntanglement/Geometry.lean:169` [status: **witness**] /-- **Proposition 6.5 (boundary witness, round-4 tie-in upgrade)**: extracts the Pythagorean identity from a `PythagoreanWitness`. The three scalars are now *committed* to boundary-fragment primitives (`kl`, `totalCorrelation`, `mfToJoint`) via three tie-in equalities — a caller can no longer satisfy the contract with arbitrary `Float`s. **Typed-API-contract disclaimer.** The analytic Pythagorean identity 30 ## Page 32 Figure 5: Every policy’s log-weight is consistent with exact linearity in 𝜆(slope error within floating-point round-off) — the numerical signature of an exponential geodesic. Four straight lines (one per policy 𝜋∈{0, 1}2) with slopes 𝐽(𝜋) −𝛾𝐾𝑐(𝜋) depart from the same point at 𝜆= 0 (the mean-field log-weight). Linearity is the e-geodesic identity Eq. (7.3) and the numerical witness of Theorem 7.4 (Lean forwarder Geometry.entangledFamily_eGeodesic). Unnormalized log-weight log ℰ𝜆(𝜋) −𝛾𝜆𝐾𝑐(𝜋) from lean.coupling.coupling_log_weight on the 31-point sweep LOG_WEIGHT_FLOW_LAMBDAS under symmetric Ising coupling with 𝐾𝑐≠0. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 31 ## Page 33 Figure 6: The K=2 Ising joint posterior, computed by lean.coupling.entangled_posterior on the 21-point linspace grid over 𝜆∈[0, 4] (simulation.hyperparameters.KL_GEODESIC_LAMBDAS), traced in a 2-D summary plane spanned by aligned-corner mass 𝑞(0, 0) + 𝑞(1, 1) (horizontal) and off-diagonal disparity |Δrow| + |Δcol| (vertical). The trace departs the mean-field anchor (red star) at 𝜆= 0 and bends toward an archetypal corner — a visual e-geodesic in the simplex coordinates used here. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 32 ## Page 34 itself (the `pythagorean` field) remains a witness payload supplied by the caller; the separate MathlibProofs layer discharges it from the KL chain rule. This theorem is **not** a stand-alone proof of the Pythagorean decomposition; it certifies that *if* a caller supplies witnesses that genuinely compute the boundary primitives, *then* the extracted identity types-check. The mathematical content lives in the manuscript appendix S01 + the Python numerical companion in [`src/lean/geometry.py`](../../src/lean/geometry.py) (which verifies the identity on randomly sampled joints + reference mean-fields). -/ theorem dualFlat_pythagorean_witness {K Pol} {q q0_star : JointDist K Pol} {mhat : MFDist K Pol} {s : List (PolicySpace K Pol)} {sumStreamEntropies : Float} (w : PythagoreanWitness q q0_star mhat s sumStreamEntropies) : w.klVal = w.tcVal + w.residual := w.pythagorean Connection to alpha-projections and curved exponential families For 𝛼∈[−1, 1], the 𝛼-projection generalizes the 𝑚(𝛼= −1) and 𝑒(𝛼= 1) projections [Amari, 2016]. The mean- field approximation in classical variational inference is m-projection of the true posterior onto ℳMF (minimize KL with 𝑞as second argument, which is what variational lower bounds compute, modulo a sign convention cataloged in §S6.1). Our 𝜆-family is the e-geodesic in the opposite direction: starting from MF and moving outward along a chosen direction. This duality is the deep reason the framework is well-behaved: we are not approximating a fixed target; we are parametrically extending the variational family to admit structure, and the m/e geometry guarantees that revertibility (back to MF) is the dual move to extension. Connection to escort distributions and deformed exponential families For non-extensive entropies (Tsallis, Rényi), one obtains escort distributions and 𝜙-deformed exponential families [Naudts, 2011, Amari, 2016]. The same construction works for 𝑞𝜆: replacing exp with a deformed exponential gives a 𝑞-deformed entanglement family. We do not develop this fully here, but flag it as a natural generalization for systems exhibiting non-extensive statistics, with an evident connection to information-theoretic measures of partial cognitive integration. Takeaways 1. The mean-field submanifold is e-flat. Mean-field policy posteriors form an e-flat submanifold of the probability simplex (Proposition 7.1); the 𝜆-family departs this submanifold along an e-geodesic (Theorem 7.4). (The boundary Lean companion checks only definitional mean-field membership; full e-flatness is the Mathlib-layer discharge target — prop_6_1 is status: proved, faithfulness: statement- restricted.) 2. Marginalization is exactly m-projection. Taking marginals is the KL-minimizing projection onto the mean-field submanifold (Proposition 7.2) — revertibility is dual to extension. (The boundary companion pins the m-projection’s KL value on the submanifold; information-projection minimality is the Mathlib-layer discharge target — faithfulness: statement-restricted.) 3. Pythagorean decomposition makes the cost explicit. Total correlation 𝐼(𝑞𝜆) equals the KL of 𝑞𝜆to its m-projection (Proposition 7.3) — the multi-information cost in the decomposition theorem is exactly the squared “distance” from the mean-field manifold in the dual geometry. Spectral Structure: Schmidt Rank, Archetypal Decomposition, and Tensor-Train Bond Profiles Bipartite Schmidt decomposition For 𝐾= 2, view 𝑞𝜆as a matrix 𝑀∈ℝ|Π1|×|Π2| with 𝑀𝑖𝑗= 𝑞𝜆(𝜋1 = 𝑖, 𝜋2 = 𝑗). Singular value decomposition: 𝑀= 𝑈Σ𝑉⊤= ∑ 𝛼 𝑠𝛼𝑢𝛼𝑣⊤ 𝛼, (8.1) 33 ## Page 35 where 𝑠𝛼≥0, 𝑢𝛼, 𝑣𝛼orthonormal. Define: • Schmidt rank 𝑟(𝑞𝜆) = #{𝑠𝛼> 0}. • Policy entanglement entropy 𝑆𝐸(𝑞𝜆) = −∑𝛼𝑝𝛼log 𝑝𝛼where 𝑝𝛼= 𝑠2 𝛼/ ∑𝛽𝑠2 𝛽. Proposition 8.1. 𝑟(𝑞𝜆) = 1 ⟺𝑞𝜆∈ℳMF (the joint distribution is a product). Equivalently, 𝑆𝐸= 0 ⟺ mean-field. The Lean companion is a live boundary statement for the rank-one / mean-field interface: -- From `lean/ActinfPolicyEntanglement/Spectral.lean:54` [status: **proved**] /-- **Proposition 7.1 (forward direction, forwarder)**: extraction shortcut for callers that already have the bipartite-mean-field predicate in hand and want the product factorization witness. -/ theorem isBipartiteMeanField_factors {Pol1 Pol2 : Type} (q : BipartiteJoint Pol1 Pol2) (h : IsBipartiteMeanField q) : ∃(u : Pol1 →Float) (v : Pol2 →Float), ∀π1 π2, q π1 π2 = u π1 * v π2 := Proposition 8.2 (witness-form). 𝑟(𝑞𝜆) is upper-semicontinuous in 𝜆. As 𝜆↑∞, 𝑟(𝑞𝜆) collapses toward the number of distinct modes of 𝐽−𝛾𝐾𝑐. As 𝜆↓0, 𝑟(𝑞𝜆) = 1. The Lean companion SpectralWitnesses.schmidtRank_upperSemicontinuous_witness is now live in the boundary fragment in witness-consuming form: the caller supplies a Schmidt-rank curve rankCurve : Float →Nat together with the mean-field anchor rankCurve 0 = 1 and the universally quantified upper-semicontinuity inequality as a structural witness, and the boundary fragment certifies the resulting existence claim by extracting the witness fields. The Mathlib4 discharge target is the semicontinuity / matrix-rank argument; the current claim is the typed witness contract plus the numerical rank sweep. The numerical realization lives in src/lean/spectral.py and is exercised by tests/test_witness_theorems.py: -- From `lean/ActinfPolicyEntanglement/SpectralWitnesses.lean:68` [status: **witness**] /-- **Proposition 8.2 (boundary witness form)**: an `UpperSemicontinuousRankWitness` *is* the existence of an upper- semicontinuous Schmidt-rank curve anchored at `rankCurve 0 = 1`. Stock Lean, zero-`sorry`. **Typed-API-contract disclaimer.** Not a stand-alone proof of upper semicontinuity; a typed-API contract. The continuity inequality is supplied as `witness.usc`; the boundary fragment re-publishes it together with the mean-field anchor. Bipartite K=2 case is now *genuinely* proved at the boundary as `Spectral.Bipartite.schmidtRankOne_iff_isBipartiteMeanField` (round 4); the general-K upper-semicontinuity statement still requires Mathlib's topological-semicontinuity library + matrix-rank lower-semicontinuity to discharge. -/ theorem schmidtRank_upperSemicontinuous_witness (rankCurve : Float →Nat) (witness : UpperSemicontinuousRankWitness rankCurve) : rankCurve 0.0 = 1 ∧∀(lam0 : Float) (r0 : Nat), rankCurve lam0 ≤r0 → ∃delta : Float, 0.0 < delta ∧ ∀lam : Float, (lam - lam0).abs < delta →rankCurve lam ≤r0 := The discontinuous-rank prediction of Proposition 8.1 is empirically observed as a step from 𝑟= 1 at 𝜆= 0 to 𝑟= 2 for any 𝜆> 0 in the K=2 Ising toy. Caveat (non-trivial coupling required). The rank jump from 1 to 2 at 𝜆= 0+ requires that 𝐽is non-trivial across the cut {1} ∣{2}, i.e. 𝐽cannot be written as 𝑓(𝜋1) + 𝑔(𝜋2) for any per-stream functions 𝑓, 𝑔. In particular, if 𝐽depends only on one stream — say 𝐽(𝜋) = 𝑓(𝜋1) — the coupling is degenerate across this cut, 𝑞𝜆remains a product across the cut for every 𝜆≥0, and rank remains 1. The Schmidt rank is computed by src/lean/spectral.py::schmidt_decomposition and gated against the analytical predictions in tests/test_spectral.py: The smooth analog, the entanglement entropy 𝑆𝐸(𝑞𝜆), takes the boundary values 𝑆𝐸(0) = −0.0000, 𝑆𝐸(1) = 0.4652, 𝑆𝐸(3) = 0.6882 and is shown across (𝜆, utility) as a heatmap below. The leading singular vectors as archetypal eigenvectors This is the formal content of the archetypal eigenvector reading of low-rank entangled posteriors. Definition (Archetypal modes). The archetypal joint policies of an entangled ensemble are the leading singular vector pairs {(𝑢𝛼, 𝑣𝛼) ∶𝑠𝛼large}. Each mode 𝛼specifies a coupled pattern: a marginal 𝑢𝛼on 𝜋1 and a co-occurring marginal 𝑣𝛼on 𝜋2, with weight 𝑠𝛼. 34 ## Page 36 Figure 7: Schmidt rank is integer-valued and steps up from 1 (mean-field manifold) to 2 as soon as 𝜆exceeds the rank-detection tolerance under pure-𝐽Ising coupling (𝐾𝑐= 0, 𝛾= 0). This step is the visual signature of the “rank-1 iff mean-field” identity Proposition 8.1 (Lean companion Spectral.Bipartite.isBipartiteMeanField_factors) and the upper-semicontinuity prediction Proposition 8.2 — a birth-of-archetype crossover at small positive 𝜆. Joint posterior built by lean.coupling.entangled_posterior; rank extracted by lean.spectral.schmidt_rank (atol = 1e-09) on the 81-point sweep SCHMIDT_RANK_LAMBDAS. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 35 ## Page 37 Figure 8: Entanglement entropy 𝑆𝐸is zero on the mean-field manifold (𝜆= 0), grows with 𝜆, then saturates as the posterior collapses onto a single archetypal mode. The saturation ceiling is utility- dependent: higher utility shifts mass toward fewer archetypes, lowering peak 𝑆𝐸. The dark band at the left edge is the visual marker of the mean-field submanifold. Computed on a 41×21 grid via lean.coupling.entangled_posterior and lean.spectral.entanglement_entropy. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 36 ## Page 38 These are not policies the agent ever literally executes — they are eigenmodes of the joint posterior. But they are interpretable as the behavioral templates the coupling structure encodes. A drummer’s “groove” is the leading (𝑢𝛼, 𝑣𝛼) pair on (left-hand-pattern, right-hand-pattern); a navigator’s “circumnavigation” pattern is a leading mode on (locomotion, gaze). This is structurally analogous to bipartite quantum entanglement entropy [Eisert et al., 2010] and to the spectral theory of probabilistic graphical models [Han et al., 2018]. In the quantum case the Schmidt coefficients {𝑐𝛼} are amplitudes of a normalized state vector with ∑𝛼|𝑐𝛼|2 = 1; in the classical-probability case here the Schmidt coefficients are singular values {𝑠𝛼} of the K=2 reshape of 𝑞𝜆, normalized by their sum-of-squares to define the spectral distribution 𝑝𝛼= 𝑠2 𝛼/ ∑𝛽𝑠2 𝛽. The analogy is mapped in tensor-network tutorials and reviews [Eisert et al., 2010, Orus, 2014] and does not promote the policy joint to a quantum state — there is no superposition, no phase, no Hilbert space; the structural similarity is at the level of the SVD-derived entropy of a bipartite array. Figure 9: A small number of Schmidt archetypes carry almost all the mass: at 𝜆= 3 the leading archetype dominates. Left panel: archetype weights {𝑠𝛼} in descending order (rank-effective is small). Right panel: overlap matrix |⟨𝑢𝑖, 𝑢𝑗⟩| ⋅|⟨𝑣𝑖, 𝑣𝑗⟩| is diagonal-dominant — archetypes are mutually orthogonal by SVD construction. Computed via lean.spectral.schmidt_decomposition at 𝜆= 3 (ARCHETYPE_DENDROGRAM_LAMBDA). Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. Multi-stream tensor decomposition For 𝐾> 2, 𝑞𝜆is a 𝐾-tensor of size ∏𝑘|Π𝑘|. Use: • CP (CANDECOMP/PARAFAC): 𝑞𝜆≈∑𝛼𝜆𝛼𝑢1 𝛼⊗𝑢2 𝛼⊗⋯⊗𝑢𝐾 𝛼. • Tucker: 𝑞𝜆≈𝒢×1 𝑈1 ×2 𝑈2 ⋯×𝐾𝑈𝐾. • Tensor train (matrix product state, MPS): 𝑞𝜆(𝜋1, … , 𝜋𝐾) ≈Tr[∏𝑘𝐴𝑘(𝜋𝑘)] with bond dimension 𝑟. Tensor-train is computationally favored: storage 𝑂(𝐾⋅|Πmax|2 ⋅𝑟2) vs ∏𝑘|Π𝑘| for the full joint, with rich expressive power for sparse/sequential coupling structure [Orus, 2014, Glasser et al., 2020, Han et al., 2018]. Definition (Multi-stream entanglement entropy). For tensor-train representation with bond dimensions {𝑟𝑘}, the maximum bond entropy across each cut {1, … , 𝑘} ∣{𝑘+ 1, … , 𝐾} is 𝑆max 𝑘 = log 𝑟𝑘. The actual bond entropy is 𝑆𝑘(𝑞𝜆) = −∑𝛼𝑝(𝑘) 𝛼 log 𝑝(𝑘) 𝛼 where {𝑝(𝑘) 𝛼 = 𝑠(𝑘),2 𝛼 / ∑𝛽𝑠(𝑘),2 𝛽 } is the spectral distribution of the bipartite reshape of 𝑞𝜆across the 𝑘-th cut; by Jensen, 𝑆𝑘(𝑞𝜆) ≤log 𝑟𝑘with equality iff the bond singular values are uniform. The full entanglement spectrum is the tuple (𝑟1, … , 𝑟𝐾−1) together with the per-cut singular-value distributions. Theorem 8.3 (Sparsity-rank tradeoff). If the coupling potential 𝐽is representable as a tensor-train with bond dimensions {𝑟𝑘} and interaction order 𝑑(the maximum order of any individual clique in the additive decomposition 𝐽= ∑𝑒𝐽𝑒), then the resulting 𝑞𝜆has tensor-train rank at most {𝑟𝑑 𝑘} on each cut (pairwise interactions give the {𝑟2 𝑘} saturation; see §D for the exact bound and the contraction exp(𝜆𝐽) = ∏𝑒exp(𝜆𝐽𝑒) that produces it). Hence sparse hierarchical coupling structures (small 𝑟𝑘, small 𝑑) yield computationally efficient posteriors, and the bond dimensions {𝑟𝑑 𝑘} are the rank of cross-cut entanglement. 37 ## Page 39 The Lean companion SpectralWitnesses.sparsityRank_tradeoff_witness is now live in the boundary fragment in witness-consuming form: the caller supplies a per-cut Schmidt-rank function and an a-priori bond- dimension envelope, together with the universally quantified rank- bound envelope, as a SparsityRankEnvelope K witness; the boundary fragment certifies that the entangled posterior respects the envelope on every cut and every 𝜆. The Mathlib4 discharge target is the tensor-product / matrix-rank proof of that envelope; the rendered Lean block below is the current source that actually builds. -- From `lean/ActinfPolicyEntanglement/SpectralWitnesses.lean:136` [status: **witness**] /-- **Theorem 8.3 (boundary witness form)**: a `SparsityRankEnvelope` witness *is* the existence of a per-cut Schmidt-rank envelope for the 𝜆-entangled posterior of a tensor-train coupling. Stock-Lean, zero- `sorry`. **Typed-API-contract disclaimer.** Not a stand-alone proof of the sparsity-rank tradeoff; a typed-API contract. The per-cut envelope `cut_rank k 𝜆≤bond_bound k` is supplied as a `SparsityRankEnvelope` field; the boundary fragment extracts it. MathlibProofs discharge from `Mathlib.LinearAlgebra.TensorProduct` plus matrix-rank bounds. -/ theorem sparsityRank_tradeoff_witness (K : Nat) (witness : SparsityRankEnvelope K) : ∀(k : Fin K) (lam : Float), witness.cut_rank k lam ≤witness.bond_bound k := This is the formal version of: the deeper the coupling structure, the higher the cross-stream rank — but sparse couplings give low rank, hence efficient inference. It directly mirrors the empirical success of MPS-based generative models [Han et al., 2018] and Friston’s renormalization-group treatment of FEP [Friston et al., 2025], in which scale-invariant generative models have an inherent sparse-coupling structure that supports efficient hierarchical inference. The bond-rank profile is computed numerically across stream counts 𝐾∈{2, 3, 4, 5} for the symmetric Ising K-stream coupling (src/simulation/builders.py::ising_coupling_tensor): TT𝐾=2 = [2], TT𝐾=3 = [2, 2], TT𝐾=4 = [2, 3, 2], TT𝐾=5 = [2, 3, 3, 2]. Figure 10: Bond dimensions stay small even as the stream count grows: 𝑟𝑗≤3 across 𝐾∈{2, 3, 4, 5}. This is the sparsity-rank tradeoff in action — low-rank Ising couplings yield low-rank posteriors, the empirical witness of Theorem 8.3. Each row of the panel is the bond-rank profile (𝑟1, … , 𝑟𝐾−1) for one stream count at 𝜆= 2. Joint built via lean.coupling.entangled_posterior over simulation.builders.ising_coupling_tensor; bond dimensions from lean.spectral.tensor_train_ranks (atol=1e-09). Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 38 ## Page 40 Birth and death of archetypes As 𝜆varies continuously from 0, the Schmidt rank can jump discontinuously upward (singular value crossings). These are the symmetry-breaking transitions of the entanglement structure — points at which a new behavioral archetype becomes available. We develop these as phase transitions in §10. Takeaways 1. Rank is the operational definition of “non-mean-field”. The joint posterior is mean-field iff its Schmidt rank is 1 (Proposition 8.1); any coupling that is non-trivial across the cut {1} ∣{2} (i.e. not of the additive form 𝑓(𝜋1) + 𝑔(𝜋2)) jumps rank to ≥2 at 𝜆> 0. (The boundary Lean companion checks the definitional rank-one / mean-field unfolding; the full rank equivalence is the Mathlib-layer discharge target — prop_7_1 is status: proved, faithfulness: statement-restricted.) 2. A few archetypes carry most of the behavioral mass. Leading singular vectors of 𝑞𝜆are the dominant cross-stream behavioral modes — the few archetypes the agent’s hyperprior repeatedly sculpts. 3. Low-rank couplings give low-rank posteriors. The sparsity-rank tradeoff (Theorem 8.3) bounds the bond dimensions of the posterior by those of the coupling — sparse hierarchical couplings yield computationally cheap inference. Heterogeneous Inference: Mixed VFE/EFE Ensembles and the Coupling-Tax Bound Three-level update hierarchy The framework induces a natural three-level hierarchy of online updates: 1. Level 1 (within-stream). Update 𝑞𝑘 𝜆for each stream, holding 𝐽, 𝐾𝑐, 𝜆fixed. 2. Level 2 (coupling structure). Update 𝐽, 𝐾𝑐as parameters of a generative model (e.g., Dirichlet-coupling for 𝐽, gradient on free energy of free energy for 𝐾𝑐). 3. Level 3 (coupling precision). Update 𝜆by gradient on 𝐹[𝑞𝜆]. Each level has a clean interpretation: - Level 1: ordinary perception/policy inference. Time scale: per-step. - Level 2: habit/preference learning. Time scale: trials to days. - Level 3: precision-like learning on the coupling itself — a model-level account of context-dependent coordination. Time scale: task phases or learning contexts. Coupled marginal updates For stream 𝑘∈𝒫(planning), the coordinate-descent update on 𝑞𝑘 𝜆is the standard fixed-point: 𝑞𝑘 𝜆(𝜋𝑘) ∝exp( log 𝐸𝑘(𝜋𝑘) −𝛾𝐺𝑘(𝜋𝑘) ⏟⏟⏟⏟⏟⏟⏟⏟⏟ single-stream EFE term + ∑ 𝑗≠𝑘 ⟨log Φ𝑘𝑗(𝜋𝑘, 𝜋𝑗)⟩𝑞𝑗 ⏟⏟⏟⏟⏟⏟⏟⏟⏟ coupling messages from other streams ) (9.1) where Φ𝑘𝑗(𝜋𝑘, 𝜋𝑗) = exp(𝜆𝐽𝑘𝑗(𝜋𝑘, 𝜋𝑗)−𝛾𝜆𝐾𝑐,𝑘𝑗(𝜋𝑘, 𝜋𝑗)). This is exactly belief propagation on a coupled factor graph with the coupling potentials Φ𝑘𝑗as factors. This recovers pymdp-style factorized inference [Heins et al., 2022] as the 𝜆= 0 limit, and generalizes it to coupled structure. The VFE-only suboptimality bound For 𝑘∈𝒱(VFE-only, reflexive), the stream takes a one-step gradient on its marginal free energy without iterative message passing. We compare to the coordinate-descent step taken by the full coupled inference. Theorem 9.1 (Heterogeneous coupling tax). Let 𝑞𝑘 ∗be the coordinate-descent step for stream 𝑘in the coupled ensemble at coupling 𝜆, and 𝑞𝑘 ∘be the one-step VFE gradient step ignoring couplings. Define the coupling magnitude ‖Φ‖∞= max𝑗,𝑘,𝜋𝑘,𝜋𝑗| log Φ𝑘𝑗(𝜋𝑘, 𝜋𝑗)|. Then: 𝐷KL(𝑞𝑘 ∗‖ 𝑞𝑘 ∘) ≤𝐶⋅𝜆2 ‖Φ‖2 ∞+ 𝑂(𝜆3) (9.2) 39 ## Page 41 for a constant 𝐶depending only on |Π𝑘| and the curvature of 𝐺𝑘. Proof sketch. Taylor-expand the coordinate-descent fixed-point equation in 𝜆around the mean-field point 𝑞𝑘 ∘. The zeroth-order term is the single-stream MF posterior; the first-order correction is the linear coupling- message contribution; the second-order term involves cross-coupling between messages from different streams. KL divergence is locally a Bregman divergence with Hessian equal to the Fisher information, 𝐷KL(𝑝‖ 𝑞) = 1 2 ‖∇log 𝑝−∇log 𝑞‖2 𝐹−1 + 𝑂(‖∇log 𝑝−∇log 𝑞‖3), so the leading correction is 𝑂(𝜆2) with prefactor controlled by ‖Φ‖2 ∞. Higher-order terms are absorbed in 𝑂(𝜆3) under the standing assumption that 𝐽and 𝐾𝑐are bounded. Cognitive interpretation. Reflexive controllers can sit inside a coupled ensemble and pay only a quadratic cost (in coupling strength) for not running the full message-passing inference. For small-to-moderate 𝜆, this is a negligible tax; for large 𝜆, the reflexive controller becomes systematically suboptimal. This gives a quantitative answer to the engineering question: how reactive can my low-level controllers be without losing the benefits of higher-level planning? Answer: reactive is fine until 𝜆2‖Φ‖2 ∞becomes comparable to the per-step free-energy budget. The 𝑂(𝜆2) envelope (see Eq. (9.2)) is verified empirically by the companion code in src/lean/heterogeneous.py (coupling_tax_within_quadratic_bound) and gated against the analytic prediction in tests/test_heterogeneous.py; for the symmetric K=2 Ising toy with the standard (J, K_c, γ, modes) of make_ising_ensemble the fitted curvature is 𝐶≈0.0575 (visualized below). Figure 11: A reflexive (VFE-only) stream pays a quadratic price for joining a planning (EFE) ensemble — the price is 𝑂(𝜆2), not 𝑂(𝜆). Numerical tax (dots) lies under the one-point-pinned 𝐶𝜆2 envelope (dashed; 𝐶pinned at the canonical probe 𝜆, not least-squares fitted) on the entire 31-point sweep 𝜆∈[0, 1.5]. This is the numerical witness of Theorem 9.1 (and its small-𝜆tolerance corollary Corollary 9.2) — a reflexive controller can ride along with a planner up to a bounded coupling-norm tax. The curvature constant 𝐶(legend) is fit at the canonical probe 𝜆from simulation.hyperparameters.COUPLING_TAX_PROBE_LAMBDA and tracks the coupling_tax_curvature_- C entry in output/data/manuscript_variables.json. Per-stream modes are pinned (VFE, EFE); tax values from lean.heterogeneous.coupling_tax(...) (Lean companion ActinfPolicyEntanglement.Heterogeneous.couplingTax_- quadratic_bound). Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. The Lean companion is the current boundary statement for the quadratic tax witness. The genuine analytic discharge is the Bregman / KL Taylor expansion, scoped to the Mathlib4 layer: -- From `lean/ActinfPolicyEntanglement/Heterogeneous.lean:61` [status: **witness**] /-- **Theorem 9.1 (boundary witness form)**: a `BoundedQuadraticTax` witness *is* the existence of the quadratic envelope. Stock-Lean, 40 ## Page 42 zero-`sorry`. **Typed-API-contract disclaimer.** This theorem is *not* a stand-alone proof of the `O(𝜆²)` coupling-tax bound; it is a typed-API contract. The analytic content — the bound `taxFunction 𝜆≤C·𝜆²` with `C ≥0` universally over `𝜆` — is supplied as a structural hypothesis (`BoundedQuadraticTax`); the boundary fragment re-publishes it as an existence claim. The Python numerical companion in [`src/lean/heterogeneous.py`](../../src/lean/heterogeneous.py) verifies the bound on concrete parameter sweeps; the separate MathlibProofs layer will discharge it from Taylor expansion of the coupling-prior log-partition. -/ theorem couplingTax_quadratic_bound (taxFunction : Float →Float) (witness : BoundedQuadraticTax taxFunction) : ∃(C : Float), 0.0 ≤C ∧ ∀lam, couplingTax taxFunction lam ≤C * lam * lam := The reflexive-stream tolerance corollary Corollary 9.2 then inverts the bound to deliver a tolerance-explicit lam_max: from Eq. (9.2), setting 𝐶𝜆2 ‖Φ‖2 ∞= 𝜀gives 𝜆max(𝜀) = √𝜀/ (𝐶‖Φ‖2∞), which is the closed form the Lean witness SmallLambdaTolerance packages. Higher-order corrections from the 𝑂(𝜆3) remainder shrink 𝜆max by a multiplicative factor that approaches 1 as 𝜀↓0, so the small-tolerance asymptotic 𝜆max ∼√𝜀is exact. -- From `lean/ActinfPolicyEntanglement/Heterogeneous.lean:106` [status: **witness**] /-- **Corollary 9.2 (boundary witness form)**: a `SmallLambdaTolerance` witness *is* the existence of the tolerance window. Stock-Lean, zero-`sorry`. **Typed-API-contract disclaimer.** Same as `couplingTax_quadratic_bound`: this is a typed-API contract, not a stand-alone proof. The continuity argument that delivers the tolerance window is supplied as a `SmallLambdaTolerance` witness; the boundary fragment re-publishes the existence claim. -/ theorem couplingTax_small_lambda_tolerance (taxFunction : Float →Float) (eps : Float) (witness : SmallLambdaTolerance taxFunction eps) : ∃(lamMax : Float), 0.0 < lamMax ∧ ∀lam, lam.abs ≤lamMax →couplingTax taxFunction lam ≤eps := Updating lambda: precision-like learning on coupling Treat 𝜆as a free parameter and minimize 𝐹[𝑞𝜆] via gradient. The cleanest expression of the gradient uses the closed exponential-family form 𝐹[𝑞𝜆] = log 𝑍𝐸(𝜆) −log 𝑍(𝜆) (§5.4 Theorem 5.5), where 𝑍𝐸is the entangled-prior normalizer and 𝑍is the joint posterior normalizer. Differentiating with the standard exponential-family identities 𝜕log 𝑍𝐸/𝜕𝜆= ⟨𝐽⟩ℰ𝜆and 𝜕log 𝑍/𝜕𝜆= ⟨𝐽−𝛾𝐾𝑐⟩𝑞𝜆gives the total gradient along the family 𝜆↦𝑞𝜆, d𝐹[𝑞𝜆] d𝜆 = ⟨𝐽⟩ℰ𝜆−⟨𝐽⟩𝑞𝜆+ 𝛾⟨𝐾𝑐⟩𝑞𝜆. (9.3) The same answer can be unpacked in the Gibbs decomposition of §5: 𝐹[𝑞𝜆] = ∑𝑘𝐹[𝑞𝑘 𝜆] + 𝛾𝜆⟨𝐾𝑐⟩𝑞𝜆+ log 𝑍𝐸(𝜆) − 𝜆⟨𝐽⟩𝑞𝜆+ 𝐼(𝑞𝜆). Holding 𝑞frozen at its current iterate gives the explicit partial 𝜕𝐹 𝜕𝜆∣ 𝑞frozen = 𝛾⟨𝐾𝑐⟩𝑞−⟨𝐽⟩𝑞+ ⟨𝐽⟩ℰ𝜆, (9.4) while the implicit chain rule along 𝑞𝜆contributes the multi-information’s 𝜆-sensitivity d𝐼(𝑞𝜆) d𝜆 = Cov𝑞𝜆(𝐽−𝛾𝐾𝑐, log 𝑞𝜆−log ̂𝑚(𝑞𝜆)). (9.5) This Fisher-style covariance has the same algebraic form as the term that drives standard precision learning, and the two paths agree term-by-term: when 𝑞𝜆minimizes 𝐹at each 𝜆along the family, the explicit and implicit pieces collapse to the closed-form gradient above. Updating 𝜆by a step of −𝜂⋅d𝐹/d𝜆is therefore precision-like learning on coupling — formally analogous to precision learning [Friston et al., 2014, Schwartenbeck et al., 2015, Limanowski et al., 2024] but scoped to cross- stream dependence rather than confidence in one stream. The model-level question is not “how confident am I in my policy?” but “how strongly should my different policies be coupled right now?” Any cognitive reading in terms of arousal, vigilance, or flexibility is a hypothesis that would need direct joint-action measurements. 41 ## Page 43 Habit accumulation and revertibility Habit learning under coupled 𝐸is straightforward Bayesian updating on 𝐽as a Dirichlet-distributed parameter [Friston et al., 2017a]: 𝐸𝜆,new(𝜋) ∝exp( ∑ 𝑘 log 𝐸𝑘(𝜋𝑘) + 𝜆𝐽new(𝜋)), 𝐽new(𝜋) = 𝐽(𝜋) + 𝛼⋅𝑞𝜆(𝜋) ⋅success_signal. (9.6) Over learning, 𝐽accumulates structure shaped by which joint policy regions repeatedly minimize 𝐺𝜆. This is a formal analog of AIF habit learning [Friston et al., 2017a] in which the updated prior is joint rather than single- stream: the manuscript claims a coupled-prior update rule and numerical habit-accumulation sidecar, not a direct biological implementation of habit formation. Revertibility. The framework distinguishes coupling-rich habit from coupling-poor (mean-field) habit. To revert a coupling-rich habit to its mean-field component, take the m-projection: 𝐸MF 𝑘 (𝜋𝑘) = ∑𝜋−𝑘𝐸(𝜋). The coupling structure 𝐽is recoverable via 𝐽= log 𝐸−∑𝑘log 𝐸MF 𝑘 (up to the normalizer). This yields an analytic decomposition of any habit into its marginal and coupled components, establishing revertibility as a structural property of the framework rather than a contingent feature. Takeaways 1. Reflexive controllers can ride along with planners — for a bounded price. The coupling tax a VFE-only stream pays for joining an EFE ensemble is 𝑂(𝜆2), not 𝑂(𝜆) (Theorem 9.1) — second-order small for small couplings. 2. The tolerance corollary makes the bound actionable. Corollary 9.2 gives a concrete coupling- norm threshold below which a reflexive stream is guaranteed to remain within a chosen tolerance of optimal — answering “how reflexive can my low-level controllers be while still benefiting from high-level planning?” 3. 𝜆is a precision-like coupling weight, learnable from free energy. Updating 𝜆by gradient on 𝐹is a formal analog of precision learning; tonic over- and under-coupling become testable hypotheses about joint-statistical signatures, not diagnostic conclusions (cf. §10). Phase Structure: Disordered, Mixed, and Frozen Coupling Regimes A note on “phase” as language. On finite policy spaces with |Π𝑘|, 𝐾< ∞the free energy 𝐹[𝑞𝜆] = log 𝑍𝐸(𝜆) −log 𝑍(𝜆) is real-analytic on [0, ∞) — it is a continuous function of a finite log-partition sum over a compact policy alphabet, so no non-analyticity is possible. True non-analyticities (the strict statistical-mechanics sense of “phase transition”) require the thermodynamic limit, i.e. 𝐾→∞or |Π𝑘| →∞. Everything in this section therefore concerns smooth crossovers on a finite system, not strict phase transitions; we use the word “phase” as a behavioral metaphor for the qualitative shifts in policy-posterior structure (Schmidt rank dropping toward 1, total correlation saturating, archetypal modes becoming dominant) that are nevertheless sharp enough to read off the relevant order parameters in practice. When we conjecture genuine phase transitions in §20 (Q1), we do so explicitly in the thermodynamic-limit setting. Phase diagram The three regimes below describe the structure of a single coupled ensemble as 𝜆varies along its axis, holding the underlying potentials 𝐽and 𝐾𝑐fixed. They should not be conflated with the bifurcation phenomenon mentioned in §5.4 and §20 (Q1), which concerns multiple optima of 𝜆↦𝐹[𝑞𝜆] that arise when (𝐽, 𝐾𝑐) are themselves incoherent. Phases live along the 𝜆axis at fixed potentials; bifurcations live in the space of potentials at the optimal 𝜆. Sweep 𝜆for fixed 𝐽, 𝐾𝑐. Three generic regimes: (I) Disordered phase, 𝜆< 𝜆(1) 𝑐. Schmidt rank 𝑟(𝑞𝜆) equals the rank of the marginal product. Total correlation 𝐼small. Behavior dominated by per-stream posteriors. Model analogy: weakly coordinated streams. Behavioral signature to test: per-stream actions are statistically independent in repeated trials — a reach is uncorrelated with the gaze direction at the moment of reach onset because each stream is sampling its own posterior. (II) Mixed phase, 𝜆(1) 𝑐 < 𝜆< 𝜆(2) 𝑐. Schmidt rank intermediate. Total correlation grows. Several archetypal modes have comparable weight. Model analogy: flexible coordinated behavior; the “sweet spot” of skilled multi-stream 42 ## Page 44 activity. Behavioral signature to test: a small repertoire of modes of coordination alternates from trial to trial — reach-with-saccade-to-target on most attempts, reach-with-saccade-elsewhere on a smaller fraction, etc., each mode internally coherent but the agent retains the option of choosing a different mode under context. (III) Frozen phase, 𝜆> 𝜆(2) 𝑐. Schmidt rank collapses to small number; one or a few archetypes dominate. Total correlation high. Behavior approaches pure archetypal joint policies. Model analogy: rigid habits or automatized routines. Behavioral signature to test: the same coupled motor program recurs across stimulus contexts — saccade and reach are stereotyped and indivisible; perturbing one stream forces a recompute of the entire joint program rather than a local correction. A schematic phase band along 𝜆with illustrative thresholds (𝜆(1) 𝑐, 𝜆(2) 𝑐) = (0.5, 2.5) for the K=2 Ising toy is shown below; the actual thresholds are model-dependent and arise from the analytic conditions stated next. Analytic conditions for the phase boundaries. On a finite system the boundaries are crossovers, not non- analyticities, but each is characterised by a derivative or gap condition on the 𝜆-trace of the spectral and entropic order parameters: • the disordered →mixed crossover 𝜆(1) 𝑐 is the smallest 𝜆≥0 at which the largest spectral gap Δspec(𝜆) = 𝑠1 −𝑠2 of the Schmidt decomposition exceeds half the bare gap of the marginal product — equivalently, the smallest 𝜆at which the effective rank 𝑟eff(𝜆) = 𝑒𝑆𝐸(𝑞𝜆) drops below 𝑟eff(0) −1; • the mixed →frozen crossover 𝜆(2) 𝑐 is the smallest 𝜆at which the effective rank drops to within a small tolerance of unity, 𝑟eff(𝜆) ≤1 + 𝜖for a chosen 𝜖∈(0, 1), equivalently the smallest 𝜆at which total correlation 𝐼(𝑞𝜆) reaches (1 −𝜖) log 𝐾(the upper bound). Both conditions reduce to one-dimensional searches on the spectral trace produced by src/lean/bernoulli_toy.py: the illustrative thresholds reflect the 𝜖= 0.1 choice on the K=2 Ising trace and shift continuously with 𝜖, the potentials 𝐽, 𝐾𝑐, and the marginal priors. In the thermodynamic limit 𝐾→∞, the same gap conditions become genuine non-analyticities; the conjectured universality classes (§20 Q3) are indexed by the rank-growth exponent of Δspec across the bipartite cut at the lower crossover. The companion alignment 𝛼(𝜆) = tanh(𝜆/2) takes the sentinel values 𝛼(0.5) = 0.2449, 𝛼(1) = 0.4621, 𝛼(2) = 0.7616, 𝛼(3) = 0.9051. Figure 12: Three coupling phases — disordered (mean-field), mixed (skilled), and frozen (archetypal) — are separated by two illustrative thresholds 𝜆(1) 𝑐, 𝜆(2) 𝑐. The disordered band (𝜆< 𝜆(1) 𝑐) is the mean- field regime: streams sample independently. The mixed band (𝜆(1) 𝑐 ≤𝜆≤𝜆(2) 𝑐) is the skilled regime: joint structure exists but the agent retains flexibility. The frozen band (𝜆> 𝜆(2) 𝑐) is the archetypal regime: the joint collapses onto a small number of dominant modes. Phases assigned by lean.bernoulli_toy.coupling_phase_at on a 401-point sweep (simulation.hyperparameters.PHASE_DIAGRAM_LAMBDAS); thresholds from PHASE_LAMBDA_C1, PHASE_- LAMBDA_C2. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. The 2-D analog across (𝜆, Δutil) exhibits the same three-regime structure as utility surplus varies; the full 41 × 21 sampled free-energy landscape is shown in the empirical suite (§13, Fig. 7), where the color minimum at each utility column traces the VFE-optimal coupling 𝜆⋆ VFE(𝑢) — a numerical quantity that should not be conflated with the 43 ## Page 45 alignment-inversion formula Eq. (6.8) in §6, which inverts the alignment correspondence rather than minimizing free energy (see the distinction made explicit in §C). Order parameters Two natural order parameters: • Largest gap: Δspec(𝜆) = 𝑠1 −𝑠2 in the spectral decomposition (distinct from the utility surplus Δutil above). Small in (I), peaks in (III), and changes most rapidly near finite-system crossover bands. • Effective rank: 𝑟eff(𝜆) = 𝑒𝑆𝐸(𝑞𝜆). Smooth indicator of phase. Model predictions and behavioral hypotheses The finite model yields three testable hypotheses for controlled joint-action tasks. They are not clinical classifications; each would require an empirical protocol that estimates 𝜆, total correlation, and the coupling-spectrum diagnostics from behavior: • Rigid, habit-dominated behavior would appear in the model as high effective coupling — high 𝜆regime, Schmidt rank near 1, behavior concentrated on one archetypal joint policy. • Poor cross-stream coordination would appear in the model as insufficient coupling — 𝜆too low, 𝐼(𝑞𝜆) near zero, streams dissociated despite intact per-stream marginals. • Skilled adaptive behavior would appear in the model as middle-regime 𝜆∼𝜆∗with a rich but not collapsed entanglement spectrum. The mechanism is the same in each case: 𝜆controls how much the joint posterior is allowed to depart from the mean- field surface, so a tonic over- or under-shoot of 𝜆shifts the archetypal spectrum without necessarily distorting any individual per-stream prior. The empirical claim is therefore narrower than a clinical diagnosis: under this model, controlled behavioral tasks would test cross-stream correlation (mutual information across modalities, between-trial joint-action repertoire, or coupling-spectrum effective rank) alongside univariate stream metrics, because the coupling account predicts the informative signal should live in the joint statistics. These hypotheses are adjacent to existing computational psychiatry accounts of precision dysregulation [Friston et al., 2014, Adams et al., 2013] and habit-vs-deliberation balance [Doll et al., 2015]. The contribution here is a candidate coupling statistic 𝜆that could be estimated or falsified from joint-action data; it is not evidence, by itself, that any named disorder is explained by coupling drift. Comparative Statics: Coupling Payoff, Two-Parameter Generalization, and Sensitivity Surfaces This section answers: given the structure of 𝐽and 𝐾𝑐, what determines whether the optimal agent has 𝜆∗> 0, and how large? The pay-off structure From the closed form Eq. (5.8) (§5.4 Theorem 5.5) and the first-derivative identity Eq. (5.9), the marginal gain at 𝜆= 0 specializes to 𝜕𝐹[𝑞𝜆] 𝜕𝜆 ∣ 0 = ⟨𝐽⟩𝐸MF −⟨𝐽⟩𝑞0 + 𝛾⟨𝐾𝑐⟩𝑞0. (11.1) The total-correlation contribution 𝜕𝐼/𝜕𝜆|0 vanishes identically because 𝐼attains its minimum at the mean-field submanifold (Proposition 7.3); the multi-information’s 𝜆-sensitivity is second-order Fisher information, not first order (Eq. (A.15)). Under the standing assumption of a centered habit potential under the bare prior, ⟨𝐽⟩𝐸MF = 0 — true by symmetry for every example in §6 and the standing convention here onward — the marginal gain reduces to 𝜕𝐹[𝑞𝜆] 𝜕𝜆 ∣ 0 = 𝛾⟨𝐾𝑐⟩𝑞0 −⟨𝐽⟩𝑞0, (11.2) so coupling pays in marginal terms when 44 ## Page 46 ⟨𝐽⟩𝑞0 > 𝛾⟨𝐾𝑐⟩𝑞0. (11.3) In words: coupling pays when the habitual cross-stream alignment is more beneficial (under the current marginal posteriors) than the EFE cost of cross-stream commitments. When the prior is asymmetric (⟨𝐽⟩𝐸MF ≠0), the inequality picks up the prior alignment ⟨𝐽⟩𝐸MF on the right — habit coupling under the posterior must exceed both the EFE cost and the prior alignment for first-order benefit. Two-parameter habit/EFE generalization The primary results in this paper use the single coupling parameter 𝜆throughout (§3, §4, §5). The two-parameter form below is recovered from the single-𝜆framework by the explicit substitution 𝐽↦(𝜆𝐸/𝜆) ⋅𝐽and 𝐾𝑐↦(𝜆𝐺/𝜆) ⋅𝐾𝑐— i.e., the dual-parameter regime is not a separate theory but a re-parameterization in which the habit and preference scales are absorbed into the coupling potentials. The corresponding structural statements (entanglement decomposition Theorem 5.1, coupled-precision log-weight geometry Theorem 7.4, and Schmidt-rank witness Proposition 8.1) carry through verbatim under this substitution. Concretely, if we allow distinct precisions on habit-coupling vs. preference-coupling: 𝑞𝜆𝐸,𝜆𝐺(𝜋) ∝∏ 𝑘 𝐸𝑘(𝜋𝑘) exp(𝜆𝐸𝐽(𝜋)) exp(−𝛾𝜆𝐺𝐾𝑐(𝜋)) exp(−𝛾∑ 𝑘 𝐺𝑘(𝜋𝑘)) (11.4) then the open question is: under what conditions on 𝐽, 𝐾𝑐does the optimal (𝜆⋆ 𝐸, 𝜆⋆ 𝐺) lie on the diagonal 𝜆𝐸= 𝜆𝐺? When it does not, the agent benefits from decoupling habit precision from preference-cost precision — habits can be maintained in a regime where preference penalties are softened, or vice versa. This suggests a computational-psychiatry modeling hypothesis rather than a validated diagnostic claim: anxiety-like overconstraint would correspond to 𝜆𝐺≫𝜆𝐸(preference-cost dominates), while habit-like automaticity would correspond to 𝜆𝐸≫𝜆𝐺. The current manuscript validates the single-parameter coefficient logic; the two-parameter locus remains a clearly marked follow-up analysis. Sensitivity to potential structure For sparse pairwise 𝐽= ∑(𝑖,𝑗)∈𝒞𝐽𝑖𝑗, the optimal 𝜆∗is determined by the spectral radius of the Fisher matrix at the MF point, evaluated on the coupling support. Rigorously: Proposition 11.1 (witness-form; live Lean companion Convexity.freeEnergy_localConcavity_at_zero_- witness). Differentiating the closed form Eq. (5.8) twice and using the standard exponential-family identity d2 log 𝑍/d𝜆2 = Var(stat) — with interchange of 𝜕/𝜕𝜆and 𝔼𝑞justified by finite-sum differentiation on the policy alphabet — gives Eq. (A.15), and at 𝜆= 0 specifically 𝜕2𝐹 𝜕𝜆2 ∣ 0 = Var𝐸MF(𝐽) −Var𝑞0(𝐽−𝛾𝐾𝑐). (11.5) The right-hand side is negative — i.e. 𝐹is locally concave at 𝜆= 0, and the mean-field baseline is a local saddle in the joint-policy direction — whenever the posterior dispersion of the combined coupling statistic exceeds the prior dispersion of the habit coupling. Two regimes make this fail: • Constant statistic. If 𝐽−𝛾𝐾𝑐is 𝑞0-a.s. constant, the right variance vanishes and 𝜕2𝐹/𝜕𝜆2|0 ≥0 — the coupling has no first-order effect. • Strongly habit-anchored prior. If the bare prior 𝐸MF already concentrates 𝐽tightly (large Var𝐸MF(𝐽)) while the per-stream EFE damps the posterior dispersion of 𝐽−𝛾𝐾𝑐, the saddle property weakens. In every other case — including all the worked examples of §6, where 𝐸MF is uniform so Var𝐸MF(𝐽) = ⟨𝐽2⟩is small relative to the posterior-amplified statistic — the mean-field baseline is a genuine saddle and some coupling pays for itself. The interesting question is therefore not whether to couple but how much, governed by the higher-order structure of 𝐹in 𝜆. The locus of 𝜆⋆(Δutil, 𝛾) for the K=2 Ising toy is shown below (Fig. 46); it sweeps sigmoidally in the utility surplus and is amplified by larger EFE precision 𝛾. 45 ## Page 47 Figure 13: Optimal coupling 𝜆⋆across (utility, 𝛾) for the K=2 Ising toy on a 20 × 16 linspace grid over [0, 0.95] × [0.5, 2] (simulation.hyperparameters.LAMBDA_STAR_UTILITIES, LAMBDA_STAR_GAMMAS). Each cell calls lean.bernoulli_- toy.optimal_lambda(np.tanh(γ·u)) so the effective surplus is modulated by the precision 𝛾. 𝜆⋆grows sigmoidally in utility surplus and is amplified by larger EFE precision 𝛾, locating the comparative-statics surface of §11. Uncertainty semantics: deterministic grid or deterministic construction; no stochastic error bars are implied. 46 ## Page 48 Part III — Formal Verification Verification in this manuscript is layered: the manuscript’s central analytical identity is machine-checked in ℝby a Mathlib4-backed Lean package; an independent stock-Lean v4.29.0 boundary fragment ships the same theorem surface as a typed API so downstream callers and the Python computational layer commit to a specific decomposition shape; and a numerical companion in src/lean/ evaluates every identity on finite ensembles to floating-point tolerance. “Machine-checked” means exactly that: Lean’s kernel has type-checked the proof object, #print axioms has been inspected on the relevant declarations, and only the three foundational axioms of Lean itself (propext, Classical.choice, Quot.sound) remain. What is proved The entanglement decomposition Theorem 5.1 is established at ℝ-level by MathlibProofs.entanglement_decomposi- tion_generalK for general 𝐾and a general entangled joint 𝑞(strict positivity and normalization the only hypotheses; 𝑞is never assumed to factorize). The proof establishes the three components the manuscript uses downstream: • non-negativity of the multi-information 0 ≤𝐷(𝑞‖ ̂𝑚(𝑞)); • the KL chain-rule identity 𝐷(𝑞‖ 𝑝) = 𝐷(𝑞‖ ̂𝑚(𝑞)) + ∑𝑖𝑞𝑖log(𝑚𝑖/𝑝𝑖); • 𝑚-projection minimality. The product-marginalization core streamMarginal_productDist and the companion finite-KL kernels (klReal_nonneg / Gibbs, klReal_split_via_intermediate, klReal_minimises_generalK) are discharged from the standing positivity + normalization hypotheses without further structural assumptions, and negative-control-verified as non-vacuous, all under the same foundational-only axiom set. The full S01 boxed identity 𝐹[𝑞𝜆] = ∑𝑘𝐹[𝑞𝑘 𝜆] + 𝛾𝜆⟨𝐾𝑐⟩+ log 𝑍𝐸(𝜆) − 𝜆⟨𝐽⟩+ 𝐼(𝑞𝜆) is then machine-checked by MathlibProofs.free_energy_decomposition_full for the genuine entangled posterior, with log 𝑍𝐸the definitional log-normalizer (not an assumed scalar), positivity and unit-mass proved (not assumed), the multi-information term discharged through the general-𝐾kernel above, and two independent negative controls. The build and axiom audit are enforced by scripts/build_mathlib_proofs.py, which runs lake build, reads #print axioms on every certified declaration, and fails the gate on any non-foundational axiom or non-empty sorryAx list. How the verification stack composes The ℝ-level proof is the verification layer. The stock-Lean v4.29.0 boundary fragment under lean/ is the typed-API layer: it ships the same theorem surface in Float arithmetic without Mathlib, with the analytic content of each statement either proved at the boundary (the algebraic identities — the four-term re-grouping, the affineness of the coupling log-weight in 𝜆, the bipartite Schmidt-rank-1 ⟺mean-field equivalence, the verdict-correctness lemma, the at-zero collapse, 𝑚-projection factorization) or carried as an explicit typed hypothesis (the analytic identities whose discharge is the ℝlayer’s job). This factoring is deliberate: it forces every downstream caller, including the separate Mathlib4 discharge layer, to commit to a specific decomposition shape and parameter-threading discipline, and it gives the stock-Lean fragment a hygiene contract (zero sorry, zero axioms beyond stock Lean, zero Mathlib dependencies, zero unsafe / partial / noncomputable) that holds independently of the analytic layer’s state. The numerical companion in src/lean/ and the pymdp harness of §14 then evaluate every identity on finite ensembles. The worst-case decomposition residual on the coupling-ablation suite is 5.55𝑒−16 — consistent with floating- point round-off at the scale of the inputs — and the dashboard invariant decomposition_lhs_eq_rhs_max_residual is regenerated on every build. The pipeline runs at Float; the proof runs at ℝ; the dashboard invariants tie the two layers to the same numerical content per run. A verified error-bounded Float↔ℝbridge — either a Flocq-style formal IEEE-754 model or an interval re-implementation — would formally tie the two layers, and is scoped at §21 as roadmap research; the present pipeline binds them empirically via the dashboard invariants. Where to read the per-row content §12 contains the per-theorem surface: the live source, the analytic content each row certifies in the boundary fragment, and the exact Mathlib4 namespace targets for the ℝdischarges. The auto-generated theorem map at docs/reference/_theorem_map.md indexes every theorem by its four-track wiring (registry label →manuscript token →Lean declaration →Python witness →test gate), and docs/reference/veridical_status.md carries the per-row status: (proved / forwarder / witness / boundary) and faithfulness: (substantive / typed-API / definitional / re-export) fields. A reader can therefore enter on any track — manuscript theorem statement, Lean source, Python witness, or test gate — and traverse to any other in one hop. The companion supplement §E reproduces the live source excerpts at chapter length so the prose →Lean traversal is single-document. One chapter follows: 47 ## Page 49 • §12 — the current theorem-proving surface, the per-row content table, the typed-API discipline that factors algebraic content from analytic payloads, and the Mathlib4 namespace targets for ongoing analytic discharge. Lean 4 Formalization: Current Boundary, Witness Contracts, and Mathlib Scope This section describes the Lean artifact that is actually built, rendered, and validated in this repository. The source of truth is the ActinfPolicyEntanglement boundary fragment under ../lean/: it compiles on stock Lean 4 v4.29.0, carries a Lean companion for every numbered theorem in this manuscript, and is re-exported through FepSketches.* for compatibility with the formalized-FEP line [Friedman, 2026c]. The section no longer prints non-current Mathlib sketch code. When the manuscript shows Lean, it shows live source extracted from lean/ActinfPolicyEntanglement/. Current Lean artifact The boundary fragment is Mathlib-free by construction and has a zero hygiene budget: 0 strict sorry, 0 axiom, 0 unsafe, 0 partial, 0 noncomputable, and 0 Mathlib imports. The current render reports 22/22 Lake jobs green over 17 boundary submodules, with 126 total Lean declarations (39 defs, 76 theorems / lemmas, 11 structures). Every numbered theorem row in manuscript/refs/labels.yaml has a live Lean companion. The companions partition into four content classes by what each one proves about the named proposition in the boundary fragment: • algebraic rows prove the named proposition outright in the boundary fragment; • definitional rows prove a sub-statement of the named proposition (the boundary-content fragment the typed API commits to), with the propositional content named beyond that sub-statement discharged at ℝ-level by MathlibProofs/; • forwarder rows re-export an already-proved boundary lemma; • typed-API rows accept the analytic payload as a typed structure field and certify the result has the registered shape (with the analytic discharge living separately — fully done for Theorem 5.1 in MathlibProofs/, named target for the rest at §20 Q14). Class Count Boundary-fragment content (named propositions; full content reference) algebraic (proved, substantive) 2 A complete machine-checked proof of the named proposition: Corollary 5.2 (coupling-verdict correctness — the Boolean decision procedure is sound) and Corollary 5.3 (the coupling log-weight vanishes pointwise at 𝜆= 0). definitional (proved, scope-restricted) 3 A machine-checked sub-statement of the named proposition: Proposition 7.1 (mfImage_isMeanField proves the definitional membership IsMeanField(mfToJoint 𝑚) — every product distribution is mean-field, by rfl; the full e-flatness statement is discharged at ℝ-level), Proposition 7.2 (mProjection_kl_eq_self_when_meanfield proves the KL equality that pins the 𝑚-projection’s value when 𝑞is already mean-field; information-projection minimality is the ℝ-level discharge), Proposition 8.1 (the definitional unfolding of the bipartite-mean-field predicate Iff.rfl-checked; the Schmidt-rank equivalence 𝑟(𝑞) = 1 ⟺ mean-field is the ℝ-level discharge target). forwarder 1 The Lean declaration re-exports an already-proved boundary lemma. 48 ## Page 50 Class Count Boundary-fragment content (named propositions; full content reference) typed-API (boundary + witness-form) 3 + 11 The Lean declaration commits the caller to a specific decomposition shape and parameter-threading discipline. 3 boundary rows fix the algebraic interface and log-weight skeleton; 11 witness-form rows accept the analytic payload (KL chain-rule identity, convexity certificate, rank semicontinuity, concentration bound) as a typed structure field. The analytic content for the central row Theorem 5.1 is established at ℝ-level in MathlibProofs/; the analytic content for the remaining typed-API rows is the discharge target of §20 Q14. The four classes are pinned per-row by the faithfulness: field in manuscript/refs/labels.yaml, audited at every render by docs/reference/veridical_status.md, and locked against silent re-inflation by tests/test_h1_headline_- invariant.py. The normative ledger of which substrate proves what is docs/reference/methods_and_assumptions.md. The typed-API class is not a hidden proof of the analytic content. It is a machine-checked contract: the caller supplies a witness field, and the boundary fragment certifies that the result has the theorem’s advertised shape. The numerical layer in src/lean/, src/simulation/, and the dashboard invariants exercises these contracts on concrete Bernoulli, Ising, pymdp, 𝐾= 3, 𝐾= 4, long-horizon, and revertibility instances; the Mathlib4 discharge layer establishes the analytic identity at the ℝlevel for the central case. What Mathlib4 is used for Mathlib4 is in scope as the analytic discharge library, not as a hidden dependency of the current boundary fragment. This separation is the most rigorous division for this project: The distinction mirrors the external toolchain rather than a local terminological preference: Lean is the proof assistant and programming language whose trusted kernel checks the boundary fragment [de Moura and Ullrich, 2021, FRO, 2026a], while Mathlib is the community mathematical library that supplies the reusable analysis, probability, algebra, and linear-algebra substrate for future and current analytic discharges [Community, 2020, FRO, 2026b]. Accordingly, a theorem row is never promoted merely because a typed witness argument exists in the boundary API; promotion requires the row-specific Lean/Mathlib source and its gate to build. Layer Current status Why this is the right boundary lean/ActinfPolicyEntanglement/ Builds without Mathlib on Lean 4 v4.29.0. Keeps the theorem registry fast, reproducible, and hygiene-auditable. Witness structures Current Lean source. Names the exact analytic payload each theorem needs without pretending it has been derived inside Mathlib. lean/MathlibProofs/ Mathlib-backed analytic discharge package; machine-checks the full S01 boxed free-energy identity (Theorem 5.1) in ℝvia free_energy_decomposition_full, with the multi-information term discharged through the axiom-clean general-𝐾kernel entanglement_decomposition_generalK. Foundational-only #print axioms (no sorryAx, two independent negative controls); enforced by scripts/build_mathlib_proofs.py and tests/test_mathlib_axiom_audit.py. Promotes Theorem 5.1 (the central result) to ℝ-verified; the Float boundary fragment in this same project is the numerically-corroborated shadow with one open residual (a verified error-bounded Float↔ℝbridge, scoped in docs/reference/methods_and_assumptions.md as multi-week future research). Manuscript + Python evidence Current, validated. Shows the analytic identities by derivation and numerical execution while the Mathlib discharge remains separate. The Mathlib target is therefore precise but non-misleading: it tells a Lean contributor where the analytic proof obligations live, while the present manuscript only claims what the current build and tests actually validate. 49 ## Page 51 Mathlib4 analytic targets The following table is not source code. It is the current dependency map from witness payload to the Mathlib4 area that should discharge it: Witness payload Boundary theorem(s) Mathlib area Finite KL / entropy chain rule Theorem 5.1, Proposition 7.3, Proposition 7.5, Proposition 19.3 PMF / finite-measure probability, finite sums, logarithms, and KL-style entropy identities Convexity and local Taylor behavior in 𝜆 Theorem 5.6, Proposition 11.1 Convex analysis, differentiability / Taylor expansion, real logarithm and exponential facts Bregman / quadratic coupling-tax envelope Theorem 9.1, Corollary 9.2 Taylor expansion plus local convex-analysis primitives; no current Mathlib Bregman divergence module is assumed Rank and spectral continuity Proposition 8.2, Theorem 8.3 Matrix rank, semicontinuity, tensor-product and finite-dimensional linear-algebra infrastructure Concentration and recursive embedding Theorem 17.1, Proposition 17.2 measure tightness, KL convergence, and recursive fixed-point infrastructure This map also explains why the boundary fragment should not import Mathlib directly. Several targets are already present in Mathlib4, several need local finite-discrete definitions on top of existing primitives, and some would require new upstream work. The current artifact remains honest by keeping those as named witness payloads instead of interleaving partial Mathlib development with the verified boundary. Two recent Mathlib infrastructure papers anchor the measure-theoretic end of this map: the Markov-kernel for- malization in MeasureTheory.Probability.Kernel.* [Degenne, 2025] supplies the kernel-composition / disintegration primitives used by KL chain-rule discharge, and the recent Brownian-motion formalization in the same namespace [Degenne et al., 2025] anchors the continuous-time infrastructure that any future extension to continuous policy spaces (currently out of scope, see §20 Q4) would build on. Both references are cited here as anchors for the witness-discharge direction, not as in-flight dependencies of the current build. Live-source injection The companion supplement §E is the executable audit trail. It does not contain hand-copied theorem blocks. Each [[LEAN: