fep-001Variational Free Energy Bound | FEP | Core Free Energy | Formalized | fep001_variationalUpperBound_eq_iff | Read invariantSurprisal plus Mathlib's native measure KL upper-bounds surprisal; for finite measures and finite surprisal, equality holds exactly when the approximate and exact posterior laws coincide. | Read assumptionsThe inequality is unconditional in ENNReal. Gap separation requires finite measures, and bound equality additionally requires surprisal below infinity so additive cancellation is sound. | Read non-vacuity reviewMatching finite posterior laws attain equality, while any unequal finite pair has a nonzero KL gap and hence a strict finite-surprisal remainder. | 3 / 2 / 1 |
|---|
fep-002Variational Evidence Bound via KL Divergence | FEP | Core Free Energy | Formalized | fep002_vfe_ge_surprisal | Read invariantVariational free energy, defined as surprisal plus Mathlib KL divergence, upper-bounds surprisal and is exact at the posterior. | Read assumptionsThe bound is unconditional over measures in a measurable space; exactness uses Mathlib's SigmaFinite assumption for KL self-divergence. The codomain is ENNReal, so infinite divergences are represented without a finiteness side condition. | Read non-vacuity reviewAny sigma-finite posterior supplies the equality witness q = posterior, while distinct measures can produce a nonzero or infinite KL remainder. | 5 / 1 / 2 |
|---|
fep-003Discounted Pragmatic Cost | Active Inference | Core Active Inference | Formalized | fep003_pragmaticCost_succ | Read invariantFinite-horizon pragmatic cost is the discounted ENNReal sum of stage costs; horizon extension exposes the exact terminal increment, costs are pointwise monotone, and horizon extension is monotone. | Read assumptionsAll costs and the discount live in ENNReal, so nonnegativity and infinity are represented directly. This is the pragmatic-cost input to EFE; epistemic value and its sign are owned by fep-021. | Read non-vacuity reviewA positive stage cost at the newly exposed time adds the nonzero increment γ^T c_T; a zero horizon and pointwise-equal costs exercise the boundaries. | 4 / 1 / 2 |
|---|
fep-004Finite Diagonal Fisher Metric | Info Geometry | Core Information Geometry | Formalized | fep004_fisherMetric_eq_zero_iff | Read invariantA finite diagonal Fisher metric is symmetric and positive semidefinite under nonnegative information weights, and becomes positive definite under strictly positive weights. | Read assumptionsThe information weights are explicit inputs rather than derived from a statistical family in this row. Positive definiteness requires every coordinate weight to be strictly positive; fep-038 computes the one-dimensional Bernoulli weight and the composed theorem identifies that specialization. | Read non-vacuity reviewAny strictly positive nonconstant weight vector and nonzero tangent has positive norm, while the zero-characterization excludes every nonzero coordinate direction. | 3 / 1 / 2 |
|---|
fep-005Four-Block State Partition | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep005_existsUnique_block | Read invariantA function-valued assignment partitions a 20-state finite space into four pairwise-disjoint blocks, and every state belongs to exactly one block. | Read assumptionsUnconditional for any assignment Fin 20 → Fin 4. This establishes an exact finite partition only; it does not infer conditional independence or identify any block as a learned Markov blanket. | Read non-vacuity reviewConstant and nonconstant assignments both instantiate the partition, while unique membership rules out overlap for every state. | 4 / 1 / 3 |
|---|
fep-006Measurable Discrete-Time Flow | FEP | Core Free Energy | Formalized | fep006_iterateFlow_add | Read invariantIteration of one measurable state update defines a measurable discrete-time flow with identity at time zero, an exact additive semigroup law, and persistence of fixed points. | Read assumptionsMeasurability of each time slice requires the one-step map to be measurable. The algebraic semigroup and fixed-point laws require no topology, invariant measure, differentiability, or continuous-time interpolation. | Read non-vacuity reviewIdentity, constant, and nontrivial measurable maps instantiate the flow; the additive law constrains every pair of horizons rather than a single composition. | 4 / 1 / 2 |
|---|
fep-007Normalized Finite Sum-Product Message | Active Inference | Core Active Inference | Formalized | fep007_normalizedMessage_sum_one | Read invariantStrictly positive local factors and incoming messages over a nonempty finite neighbor support define a nonnegative normalized sum-product message with support mass exactly one. | Read assumptionsNormalization requires a nonempty selected support and strict positivity of every factor and incoming message on it. The message is zero outside that support. This is one exact local update, not loopy-belief-propagation convergence or global marginal correctness. | Read non-vacuity reviewSingleton and multi-neighbor supports produce positive normalizers; unequal factor-message products yield a genuinely nonuniform normalized message. | 7 / 3 / 4 |
|---|
fep-008Finite Policy Objective Minimizer | Active Inference | Core Active Inference | Formalized | fep008_exists_minG | Read invariantA real-valued objective attains a minimum on a finite nonempty policy set. | Read assumptionsExistence requires only a finite nonempty policy set and an explicit real-valued objective. The theorem does not claim uniqueness of the policy; it separately proves that all minimizers agree in value. | Read non-vacuity reviewA policy set with at least two policies and unequal objective values has a genuine selected minimizer; tied objectives exercise nonunique policies with equal minimum value. | 4 / 0 / 4 |
|---|
fep-009Conditional Independence Laws | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep009_condIndep_symm | Read invariantConditional independence of two σ-algebras given a third is symmetric under Mathlib's conditional-expectation-kernel definition. | Read assumptionsConditional on a standard Borel measurable space, a finite measure, a conditioning σ-algebra below the ambient one, and the stated conditional-independence relation. The theorem is a law of conditional independence, not a learned Markov-blanket factorization. | Read non-vacuity reviewfep009_condIndep_bot_right proves that every σ-algebra is conditionally independent of the trivial σ-algebra, so the relation is inhabited. | 7 / 0 / 1 |
|---|
fep-010Detailed Balance Implies Invariance | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep010_reversible_invariant | Read invariantA Markov kernel satisfying measure-theoretic detailed balance leaves its reference measure invariant. | Read assumptionsConditional on Mathlib's IsMarkovKernel instance and IsReversible flow equality over all measurable set pairs. This proves stationarity, not a path-space fluctuation theorem or convergence to equilibrium. | Read non-vacuity reviewfep010_identity_reversible and fep010_identity_invariant provide a concrete reversible Markov-kernel witness for every measure. | 5 / 0 / 1 |
|---|
fep-011Surprise and Self-Information | FEP | Core Free Energy | Formalized | fep011_surprise_eq_zero_iff | Read invariantNegative-log self-information is nonnegative on positive probabilities at most one, additive on positive products, strictly antitone, and zero exactly at certainty. | Read assumptionsPositivity excludes the logarithmic boundary, and the probability interpretation additionally uses p≤1. Additivity is scalar and corresponds to product probabilities; no independence relation is inferred by the theorem. | Read non-vacuity reviewEvery p in (0,1) has strictly positive surprise, p=1 is the unique zero, and two positive factors exercise the additive law. | 7 / 1 / 1 |
|---|
fep-012Finite Policy Shannon Entropy Regularization | FEP | Core Free Energy | Formalized | fep012_entropyRegularizedCost_le_expectedCost | Read invariantFinite Shannon policy entropy is nonnegative on unit-interval weights, vanishes for point policies, and at nonnegative temperature lowers expected cost by exactly its entropy reward. | Read assumptionsEntropy nonnegativity only requires each weight in [0,1]; normalization is supplied separately by a policy law such as fep-028 softmax. The theorem compares objectives and does not claim that softmax is the unique optimizer. | Read non-vacuity reviewA point mass has zero entropy while a multi-policy interior law has positive terms; positive temperature yields a nonzero objective correction whenever entropy is positive. | 7 / 3 / 4 |
|---|
fep-013Equilibrium Helmholtz Differential Identities | Thermodynamics | Core Thermodynamics | Formalized | fep013_helmholtz_derivative_eq_neg_entropy | Read invariantFor differentiable U(T) and S(T), Helmholtz free energy has derivative U'−S−TS'; under the equilibrium first-law identity U'=TS', this reduces exactly to dF/dT=−S. | Read assumptionsThe derivative law is conditional on pointwise differentiability and the explicitly stated equilibrium identity. It is a thermodynamic calculus identity, not a derivation of the first law or an identification with variational free energy. | Read non-vacuity reviewThe fep-040 Gaussian thermal entropy with U(T)=T/2 satisfies the premise at every positive temperature, yielding a compiled nonconstant physical witness. | 6 / 1 / 3 |
|---|
fep-014KL Divergence: Non-Negativity, Identity, and Chain Rule | Info Geometry | Core Information Geometry | Formalized | fep014_kl_chain_rule | Read invariantMathlib KL divergence is nonnegative, vanishes exactly on equal finite measures, and obeys the composition-product chain rule for Markov kernels. | Read assumptionsSelf-divergence uses SigmaFinite; zero-characterization and the chain rule use finite measures; the chain rule additionally requires Markov kernels. The pin separately exposes native measure-KL data processing under a Markov kernel as InformationTheory.klDiv_comp_right_le; fep-014 does not include that theorem in its maintained theorem surface. | Read non-vacuity reviewEqual finite measures witness zero KL, unequal finite measures exercise the zero-characterization, and distinct Markov kernels give a nontrivial conditional term in the chain rule. | 4 / 0 / 1 |
|---|
fep-015Measurable Variational Integrand | FEP | Core Free Energy | Formalized | fep015_variationalIntegrand_measurable | Read invariantA pointwise variational integrand built from measurable energy, approximate log density, and generative log density is measurable and remains so under measurable reparameterization and baseline shifts. | Read assumptionsAll three real-valued ingredients and any reparameterization are assumed measurable. Measurability does not imply integrability, finite expectation, or existence of an optimizer, none of which is claimed. | Read non-vacuity reviewNonconstant measurable coordinate functions instantiate all three terms, and a nonidentity measurable reparameterization exercises the composition theorem. | 3 / 1 / 1 |
|---|
fep-016Exact Scalar Quadratic Laplace Kernel | FEP | Core Free Energy | Formalized | fep016_laplaceKernel_integral | Read invariantA positive-precision scalar quadratic exponential is integrable and has the exact Gaussian normalizing integral sqrt(π/(precision/2)). | Read assumptionsPrecision is strictly positive for the scientific integrability result. This is the exact scalar quadratic case underlying Laplace approximation; no approximation-error or higher-dimensional determinant theorem is claimed. | Read non-vacuity reviewAt precision two the kernel is exp(−x²) with normalizer sqrt(π), and every positive precision gives a nonconstant integrable density kernel. | 7 / 1 / 1 |
|---|
fep-017Posterior Kernel Reconstruction | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep017_posterior_joint_reconstruction | Read invariantMathlib's posterior is a Markov kernel whose composition with the predictive law reconstructs the swapped prior-likelihood joint law; for a Markov likelihood it also recovers the prior. | Read assumptionsConditional on standard-Borel and nonempty latent structure plus finite prior and likelihood kernel. The Radon--Nikodym Bayes formula additionally uses countability of the latent space and standard-Borel observation structure. This is a regular posterior-kernel theorem, not a claim about learned or approximate posteriors. | Read non-vacuity reviewEvery posterior fibre has mass one, and the identity Markov kernel supplies a concrete prior-recovery witness; non-deterministic finite kernels exercise a nontrivial reconstructed joint law. | 4 / 1 / 1 |
|---|
fep-018Bernoulli Fisher–Rao Coordinate Distance | Info Geometry | Core Information Geometry | Formalized | fep018_fisherRaoDistance_eq_zero_iff | Read invariantThe Bernoulli Fisher--Rao coordinate distance is nonnegative, symmetric, separating on the probability interval, and satisfies the triangle inequality. | Read assumptionsSeparation is restricted to Bernoulli parameters in [0,1], where square root and arcsine are injective. This is the closed-form one-dimensional Fisher--Rao distance, not a general geodesic-existence theorem for arbitrary statistical manifolds. | Read non-vacuity reviewThe endpoint parameters p = 0 and q = 1 have distinct coordinates, while every equal pair has zero distance. | 4 / 2 / 3 |
|---|
fep-019Prior-Predictive Kernel Composition | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep019_priorPredictive_assoc | Read invariantThe native prior-predictive law preserves total mass for a Markov likelihood and sequential prediction equals measure composition by the composed kernels. | Read assumptionsMass preservation requires a Markov likelihood; probability mass one additionally requires a probability prior. The associativity law is structural measure-kernel composition and does not assert model calibration or identifiability. | Read non-vacuity reviewA probability prior and non-deterministic finite Markov likelihood yield a normalized non-Dirac predictive law; a second kernel exercises genuine sequential composition. | 3 / 1 / 1 |
|---|
fep-020Two-State Markov Relaxation | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep020_tendsto_uniform | Read invariantA normalized symmetric two-state transition has the uniform stationary law; its exact n-step deviation is (1-2α)^n times the initial deviation and converges to zero for 0 < α < 1. | Read assumptionsTransition nonnegativity uses α in [0,1], while convergence uses the strict interior so |1-2α| < 1. This is an exact finite-state Markov relaxation model, not a discretized Langevin diffusion. | Read non-vacuity reviewFor α = 1/4 and any nonstationary initial mass, deviations contract geometrically by 1/2 at every step; at α = 1 the chain instead alternates and the strict-interior convergence premise excludes it. | 7 / 2 / 4 |
|---|
fep-021EFE Epistemic–Pragmatic Balance | Active Inference | Core Active Inference | Formalized | fep021_efe_epistemic_balance | Read invariantExpected free energy is pragmatic expected cost minus epistemic information value in ENNReal; under epistemic value at most cost, adding information back reconstructs cost, while EFE is monotone in cost and antitone in information. | Read assumptionsThe truncated subtraction convention makes EFE nonnegative and requires an explicit epistemic≤pragmatic premise for exact reconstruction. It does not assert the alternative risk-plus-ambiguity identity without a generative-model derivation. | Read non-vacuity reviewStrictly positive pragmatic cost with zero information yields positive EFE, equal cost and information yields zero, and intermediate information lowers EFE without changing sign. | 5 / 1 / 1 |
|---|
fep-022Posterior-Predictive Kernel and Brier Properness | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep022_brier_eq_optimum_iff | Read invariantMarkov posterior and likelihood kernels compose into normalized posterior-predictive fibres, and expected Bernoulli Brier loss is uniquely minimized by the true event probability. | Read assumptionsKernel normalization requires both components to be Markov. Brier properness is an exact real-algebra identity whose probabilistic interpretation restricts true and forecast masses to [0,1]. It is a proper one-event discrepancy, not an empirical calibration-frequency theorem. | Read non-vacuity reviewNon-deterministic posterior and likelihood kernels produce nontrivial predictive true-event mass; every forecast q distinct from p incurs the strictly positive squared regret (q-p)^2. | 4 / 3 / 2 |
|---|
fep-023Policy-Indexed Reachable Laws | Active Inference | Core Active Inference | Formalized | fep023_reachable_normalized | Read invariantThe distributional affordance set is the image of available policies under their outcome-law map; policy-set inclusion is monotone and normalization of every policy law transfers to every reachable law. | Read assumptionsReachability is policy-indexed one-step image semantics. Normalization is an explicit premise on available policy laws; no controllability, multi-step support closure, or topology on the law space is claimed. | Read non-vacuity reviewDistinct policies may induce distinct normalized measures, while an empty policy set yields no reachable law and a singleton set yields its single law. | 4 / 1 / 1 |
|---|
fep-024KL Regularization in Objectives | Info Geometry | Core Information Geometry | Formalized | fep024_klRegularizedObjective_exact | Read invariantAn ENNReal objective regularized by a nonnegative weight times native measure KL upper-bounds its base, is monotone in weight, recovers the base at zero weight, and is exact when approximation equals a sigma-finite prior. | Read assumptionsThe codomain explicitly admits infinite objectives and KL values. Exactness at the prior uses sigma-finiteness; no differentiability or optimizer-existence claim is made. | Read non-vacuity reviewPositive weight and unequal finite laws contribute a nonzero regularizer, while zero weight and matching laws independently exercise both exactness mechanisms. | 4 / 1 / 1 |
|---|
fep-025Conserved Nonequilibrium Probability Currents | Thermodynamics | Core Thermodynamics | Formalized | fep025_cycleCurrent_stationary | Read invariantFor flux πᵢPᵢⱼ, forward-minus-reverse current is antisymmetric; row normalization plus π-stationarity derives zero divergence. A directed three-state transition with uniform stationary law has a nonzero divergence-free current. | Read assumptionsThe general stationarity theorem explicitly requires normalized transition rows and a stationary real mass vector. The concrete witness is a finite deterministic cycle; no continuous-state NESS existence or thermodynamic force law is inferred here. | Read non-vacuity reviewThe clockwise three-state transition is nonidentity, preserves the uniform law, has current 1/3 on edge 0→1, and nevertheless has zero divergence at every state. | 8 / 6 / 3 |
|---|
fep-026Negative-Log Prior Complexity | FEP | Core Free Energy | Formalized | fep026_priorComplexity_eq_zero_iff | Read invariantNegative-log prior complexity is additive on positive product densities, strictly antitone, and zero exactly at unit density. | Read assumptionsThe input is a positive scalar prior-density value, not a normalized prior measure. Product additivity is exact; measure-valued relative complexity is owned by fep-014 and fep-024. | Read non-vacuity reviewEvery density in (0,1) has positive complexity, unit density is the unique positive zero, and unequal positive values exercise strict antitonicity. | 7 / 1 / 1 |
|---|
fep-027Hierarchical Kernel Factorization | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep027_hierarchical_assoc | Read invariantA parent measure and child kernel form a normalized hierarchical joint whose marginals recover the parent and prior predictive, and whose three-level factorization is associative up to product reassociation. | Read assumptionsJoint normalization requires a probability parent and Markov child; first- and second-marginal identities require the stated finite-kernel classes. The associativity theorem is exact for Mathlib composition products and does not impose causal identifiability. | Read non-vacuity reviewA non-Dirac finite parent and state-dependent non-deterministic Markov child give a dependent normalized joint with distinct parent and predictive marginals; a third kernel exercises nontrivial reassociation. | 4 / 1 / 1 |
|---|
fep-028Support-Aware Finite Softmax Policy | Active Inference | Core Active Inference | Formalized | fep028_softmax_sum_univ | Read invariantExponentiated policy scores on a nonempty selected support define a nonnegative full finite weight vector, vanish outside support, are pointwise at most one, and sum to one globally. | Read assumptionsOnly support nonemptiness is required; inverse temperature and costs may be arbitrary reals. This proves an exact stochastic policy law but not optimality, sampling behavior, or a temperature limit. | Read non-vacuity reviewA two-policy support with unequal costs gives unequal positive weights, while excluded policies have exact zero mass and the full ten-policy vector remains normalized. | 7 / 1 / 2 |
|---|
fep-029Quadratic Bregman Divergence | Info Geometry | Core Information Geometry | Formalized | fep029_quadraticBregman_eq_zero_iff | Read invariantThe scalar Bregman divergence generated by φ(x)=x² equals (x-y)², is nonnegative, and vanishes exactly when x=y. | Read assumptionsUnconditional over real x and y for the explicit quadratic generator; no general differentiable convex function, projection theorem, or mirror-descent convergence is claimed. | Read non-vacuity reviewAt x=1 and y=0 the divergence equals 1; at x=y it equals 0. | 7 / 1 / 2 |
|---|
fep-030Maximum Entropy Principle | Thermodynamics | Core Thermodynamics | Formalized | fep030_binaryEntropy_max | Read invariantBinary Shannon entropy in nats is globally at most log 2, with equality exactly at probability one half. | Read assumptionsThe native Mathlib theorem is unconditional over real inputs because Real.binEntropy has a total extension; the scientific probability domain is [0,1]. This is the Bernoulli maximum-entropy principle, not the general constrained Jaynes problem. | Read non-vacuity reviewThe equality characterization proves attainment at p = 1/2 and strict loss at every other real input. | 6 / 0 / 4 |
|---|
fep-031Finite Boltzmann–Gibbs Weights | Thermodynamics | Core Thermodynamics | Formalized | fep031_gibbsProbability_sum_one | Read invariantPositive exponential Gibbs weights normalize to a nonnegative mass function summing to one on any nonempty finite support. | Read assumptionsConditional only on a nonempty selected support; β and energies are arbitrary reals. The row does not derive Gibbs weights from maximum entropy or bundle the result as a measure. | Read non-vacuity reviewA singleton support has normalized mass one, while two unequal energies produce distinct positive normalized weights. | 5 / 1 / 1 |
|---|
fep-032Exact Quadratic Gradient-Descent Dynamics | FEP | Core Free Energy | Formalized | fep032_quadraticUpdate_tendsto | Read invariantGradient descent on the centered scalar quadratic has an exact n-step iterate, nonincreasing energy for step sizes in [0,2], and converges globally to the center for steps in (0,2). | Read assumptionsThe closed form is unconditional. Energy descent uses 0≤η≤2 and convergence uses the strict stability interval 0<η<2. This is an exact quadratic model, not a theorem for arbitrary smooth or convex objectives. | Read non-vacuity reviewAt η=1/2 every displacement halves, producing nontrivial geometric convergence; η=1 reaches the center in one step and the endpoints expose the non-strict boundary. | 5 / 1 / 2 |
|---|
fep-033Finite-Horizon Bellman Recursion | Active Inference | Core Active Inference | Formalized | fep033_bellman | Read invariantA deterministic transition-aware finite-horizon value obeys an exact Bellman recursion with stage cost, discount, and terminal cost; it is monotone in both cost functions and has exact zero-cost and zero-discount boundaries. | Read assumptionsThe transition is deterministic and the codomain is ENNReal. No stochastic policy optimization, discount-convergence limit, or infinite-horizon fixed point is claimed. | Read non-vacuity reviewA nonconstant transition and positive discount propagate later-state terminal and stage costs, while zero discount isolates the immediate cost exactly. | 4 / 1 / 1 |
|---|
fep-034Normalized Bayesian Filtering | Active Inference | Core Active Inference | Formalized | fep034_filter_joint_reconstruction | Read invariantA transition-composed predictive prior and native observation posterior reconstruct the swapped predicted-state/observation joint law, with probability mass one in every posterior fibre. | Read assumptionsConditional on standard-Borel nonempty latent structure, a finite prior, and finite transition and observation kernels; prediction preserves total mass when the transition is Markov, and posterior recovery additionally requires a Markov observation kernel. This is a one-step exact filter, not a convergence or learned-state theorem. | Read non-vacuity reviewA nonidentity finite Markov transition followed by a noisy observation kernel yields a nontrivial predictive prior and posterior; each posterior fibre has mass one rather than merely nonnegative unnormalized weight. | 4 / 2 / 1 |
|---|
fep-035Jensen's Inequality for Log | FEP | Core Free Energy | Formalized | fep035_log_jensen_two_strict | Read invariantFor distinct positive inputs and strictly positive weights summing to one, the weighted average of logarithms is strictly below the logarithm of the weighted average. | Read assumptionsConditional on x,y > 0, x ≠ y, a,b > 0, and a+b=1. This is the exact two-point strict Jensen law; finite-family and measure-integral variants are not claimed. | Read non-vacuity reviewWitnessed by x = 1, y = 2, and a = b = 1/2. | 7 / 0 / 1 |
|---|
fep-036Laplace-Smoothed Empirical Bernoulli Prior | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep036_smoothedRate_tendsto_of_empiricalRate | Read invariantA Mathlib finite binomial sampling law supplies admissible success counts; Laplace smoothing maps every outcome to an interior Bernoulli prior, is monotone in successes, and preserves the limit of any convergent empirical-frequency sequence. | Read assumptionsThe finite sampling law requires p in [0,1]. Interiority uses the intrinsic count bound, and consistency transfer explicitly assumes convergence of the raw empirical frequency. The row does not prove the binomial law of large numbers, a finite-sample risk bound, or marginal-likelihood hyperparameter optimality. | Read non-vacuity reviewEvery count in Fin (n+1) is admitted by the estimator; zero successes in zero trials gives 1/2, nontrivial counts vary within (0,1), and the shrinkage factor tends to one while the pseudocount offset tends to zero. | 8 / 4 / 4 |
|---|
fep-037Two-State Correlation–Response Law | Thermodynamics | Core Thermodynamics | Formalized | fep037_response_eq | Read invariantFor the symmetric two-state relaxation eigenvalue 1-2α, stationary autocorrelation obeys an exact recurrence and decays for 0<α<1; the discrete fluctuation--response kernel equals 2βα variance times the same geometric mode and also decays. | Read assumptionsResponse is defined as inverse temperature times the one-step autocorrelation loss. Nonnegativity additionally restricts α≤1/2 and nonnegative inverse temperature and variance. This is an exact discrete two-state response law, not a microscopic Kubo derivation for general dynamics. | Read non-vacuity reviewFor α=1/4, positive β, and nonzero variance, lag-zero response is positive and both correlation and response decay geometrically by 1/2. | 5 / 3 / 2 |
|---|
fep-038Bernoulli Fisher Information and Natural Gradient | Info Geometry | Core Information Geometry | Formalized | fep038_fisherInformation_eq | Read invariantThe differentiated Bernoulli family has zero expected score and Fisher information 1/(p(1-p)); its inverse metric defines a dual natural gradient and is the pullback of the Euclidean metric along the Fisher--Rao coordinate. | Read assumptionsMetric positivity, inverse-metric duality, and the coordinate law require an interior Bernoulli parameter 0 < p < 1. This is a complete one-dimensional Bernoulli information geometry, not a general finite- or infinite-dimensional statistical manifold. | Read non-vacuity reviewAt p = 1/2 the Fisher information is 4, every nonzero tangent has positive metric norm, and the natural-gradient map rescales nonzero covectors by 1/4. | 8 / 7 / 5 |
|---|
fep-039Four-Block Additive Free Energy | FEP | Core Free Energy | Formalized | fep039_global_eq_zero_iff | Read invariantFour local free-energy contributions aggregate additively and monotonically; under local nonnegativity, their global sum vanishes exactly when every local term vanishes. | Read assumptionsAdditivity is unconditional over four real components. Zero separation requires each local term to be nonnegative. The composed partition theorem ties those four components to fep-005's exact state blocks. | Read non-vacuity reviewA single positive local contribution makes the global quantity positive, while independent nonzero contributions exercise exact additivity. | 5 / 1 / 3 |
|---|
fep-040Native Gaussian Law and Thermal Entropy Response | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep040_thermalEntropy_hasDerivAt | Read invariantMathlib's real Gaussian law is normalized with its stated mean and variance; the one-dimensional closed-form entropy is strictly variance-monotone, differentiable with derivative 1/(2v), and under v=κT has derivative 1/(2T) and heat capacity 1/2. | Read assumptionsThe native probability, mean, and variance theorems include the zero-variance Dirac boundary. Entropy monotonicity and derivatives require positive variance, and the thermal relation requires κ,T>0. The closed-form entropy is specified directly rather than rederived here as an integral of negative log density. | Read non-vacuity reviewFor unit scale and positive temperature, the Gaussian law is nondegenerate, its entropy response is nonzero, and the dimensionless heat capacity is exactly 1/2. | 7 / 5 / 3 |
|---|
fep-041Expected Information Gain via Measure KL | Active Inference | Core Active Inference | Formalized | fep041_expectedInformationGain_zero | Read invariantInformation gain is native measure-valued KL divergence: it is nonnegative, separates finite posterior and prior measures, and its predictive expectation vanishes when observations leave the posterior unchanged almost everywhere. | Read assumptionsKL separation requires finite measures. The zero expected-information theorem requires a sigma-finite prior and almost-everywhere posterior equality; it does not claim that every informative experiment has strictly positive expected gain. | Read non-vacuity reviewAn observation-independent posterior equal to the prior yields zero gain, while any unequal finite posterior/prior pair has nonzero KL by separation. | 3 / 2 / 2 |
|---|
fep-042Bernoulli Sufficient-Statistic Factorization | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep042_likelihood_eq_of_stat_eq | Read invariantThe Bernoulli sequence likelihood factorizes exactly through success and failure counts, so samples with equal count statistics have identical likelihood for every parameter. | Read assumptionsThe theorem is finite-sample and algebraic over a Boolean observation list. Its probabilistic interpretation restricts p to [0,1]; no completeness, asymptotic efficiency, or non-Bernoulli family is claimed. | Read non-vacuity reviewDistinct orderings such as [true,false] and [false,true] have the same statistic and likelihood, while samples with different success counts generally differ for interior p. | 2 / 4 / 2 |
|---|
fep-043Fermat Criticality and Quadratic Curvature | FEP | Core Free Energy | Formalized | fep043_quadratic_critical_iff | Read invariantFermat's theorem makes every local minimum critical; for an exact positive-curvature quadratic, the derivative is the stated gradient, the center is the unique critical point and global minimizer, and the scalar Hessian is strictly positive. | Read assumptionsThe general derivative-zero theorem uses Mathlib's local-minimum notion. Uniqueness and positive second derivative are proved only for the explicit scalar quadratic with a>0, not inferred for arbitrary differentiable objectives. | Read non-vacuity reviewEvery positive a and noncenter x has nonzero gradient and strictly larger energy than the center, while the Hessian 2a is nonzero everywhere. | 6 / 2 / 4 |
|---|
fep-044Bernoulli Squared Hellinger Divergence | Info Geometry | Core Information Geometry | Formalized | fep044_hellingerSq_eq_zero_iff | Read invariantThe squared Hellinger divergence between Bernoulli laws is nonnegative, symmetric, invariant under success/failure relabeling, and separates parameters on [0,1]. | Read assumptionsNonnegativity and symmetry are unconditional for the real-valued formula; the probability-divergence interpretation and separation theorem restrict both parameters to [0,1]. This is the Hellinger member of the alpha-divergence family, not a theorem for every alpha. | Read non-vacuity reviewEqual Bernoulli parameters have zero divergence, while the endpoint laws p = 0 and q = 1 are separated. | 4 / 1 / 2 |
|---|
fep-045Finite Bernoulli Conjugate Closure | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep045_bernoulli_posterior_closed | Read invariantFor a nonzero evidence normalizer, likelihood-times-Bernoulli-prior mass normalizes pointwise to another Bernoulli law at the Bayes-updated parameter. | Read assumptionsClosure is exact for a binary latent hypothesis and binary evidence likelihood. Interior prior and positive likelihood assumptions prove positive evidence and keep the updated parameter in [0,1]. This is a finite Bernoulli conjugate family, not Beta-density conjugacy. | Read non-vacuity reviewUnequal positive likelihoods move an interior prior parameter while posterior mass still sums to one; equal likelihoods leave the prior parameter unchanged algebraically. | 4 / 4 / 2 |
|---|
fep-046Finite Stick-Breaking Mass Conservation | Bayesian Mechanics | Core Bayesian Mechanics | Formalized | fep046_mass_conservation | Read invariantFor every finite stick-breaking sequence, allocated weights plus residual mass equal exactly one; unit-interval breaks keep the residual in [0,1]. | Read assumptionsMass conservation is a purely algebraic identity with no bounds. Residual nonnegativity and the unit upper bound require every break fraction in [0,1]. No infinite-series exhaustion or random-process law is claimed. | Read non-vacuity reviewMultiple unequal interior breaks allocate several positive weights and a positive remainder, while a break of one exhausts all subsequent residual mass. | 3 / 2 / 2 |
|---|
fep-047Compositional Finite Sum-Product Propagation | Active Inference | Core Active Inference | Formalized | fep047_forward_compose | Read invariantFinite sum-product forward propagation is matrix--vector multiplication: it preserves nonnegativity and order under nonnegative factors, has zero and identity laws, and composes exactly by matrix multiplication. | Read assumptionsNonnegativity and monotonicity require entrywise nonnegative factors and inputs. Identity and composition are unconditional algebraic laws. The row proves exact finite propagation, not normalization or loopy fixed-point convergence. | Read non-vacuity reviewNonidentity dense matrices and nonconstant incoming vectors exercise genuine cross-state aggregation; two distinct factors exercise nontrivial composed propagation. | 5 / 1 / 2 |
|---|
fep-048Contractive Policy Update Uniqueness | FEP | Core Free Energy | Formalized | fep048_contraction_unique | Read invariantMathlib's global ContractingWith contract gives a unique fixed point on ℝ, and iterations of the concrete halving update converge to zero. | Read assumptionsContractingWith packages a nonnegative Lipschitz coefficient strictly below one. Completeness and nonemptiness of ℝ discharge the Banach fixed-point assumptions; no claim is made for arbitrary noncontractive policy updates. | Read non-vacuity reviewThe nonconstant update x ↦ x/2 is certified with coefficient 1/2, has zero as its unique fixed point, and has iterates converging to zero from every real start. | 8 / 1 / 3 |
|---|
fep-049Linear Constitutive Entropy Production | Thermodynamics | Core Thermodynamics | Formalized | fep049_entropyProduction_eq_zero_iff | Read invariantUnder Jᵢ=LᵢXᵢ, the flux--force pairing is a nonnegative quadratic form that separates equilibrium for Lᵢ>0. Independently, positive forward/reverse edge fluxes have production (f-r)log(f/r)≥0, with equality exactly at detailed balance. | Read assumptionsThe finite constitutive law is diagonal and assumes nonnegative conductances. The edge theorem assumes strictly positive bidirectional fluxes so affinity is finite. Cross-coupled Onsager matrices and microscopic derivations remain outside the claim. | Read non-vacuity reviewAny nonzero force under positive conductance produces positive quadratic entropy; unequal positive directed fluxes produce positive edge entropy, while equality of fluxes is the exact zero-production boundary. | 5 / 4 / 3 |
|---|
fep-050Logical Erasure and the Landauer Bound | Thermodynamics | Core Thermodynamics | Formalized | fep050_landauer_work_bound | Read invariantA noninjective reset maps an unbiased bit to a pure state and loses exactly kB log 2 entropy; nonnegative total entropy at positive temperature derives the corresponding heat bound, and work above heat derives the work bound. | Read assumptionsThe derivation explicitly assumes the second-law total-entropy inequality, positive environmental temperature, and work at least as large as dissipated heat. It does not model a microscopic Hamiltonian or finite-time erasure protocol. | Read non-vacuity reviewThe reset identifies true and false, the unbiased-to-pure entropy change is exactly nonzero for kB > 0, and equality in the environmental balance saturates the Landauer threshold. | 5 / 6 / 2 |
|---|
fep-051Likelihood-Ratio Reconstruction under Absolute Continuity | Bayesian Mechanics | Measure Bayesian Inversion | Formalized | fep051_likelihoodRatio_reconstruction | Read invariantA native Radon–Nikodym derivative reconstructs a target measure from its reference exactly when the target is absolutely continuous with respect to that reference. | Read assumptionsBoth results require a measurable carrier and a HaveLebesgueDecomposition instance. The forward reconstruction additionally assumes target ≪ reference; the equivalence proves that this is the exact support condition and does not erase a singular component. | Read non-vacuity reviewTaking target equal to reference supplies a reconstructible case, while any target with a nonzero singular component lies on the theorem's explicit failure boundary. | 2 / 0 / 1 |
|---|
fep-052Posterior Density as a Likelihood Tilt | Bayesian Mechanics | Measure Bayesian Inversion | Conditional Proxy | fep052_posterior_density_tilt | Read invariantA posterior kernel is a prior measure tilted by the likelihood-to-predictive Radon–Nikodym derivative for predictive-almost-every observation. | Read assumptionsThe native result assumes a finite prior, a finite likelihood kernel, a nonempty standard-Borel parameter space, countable generation between the parameter and observation spaces, and prior-almost-every likelihood domination. The countable specialization discharges domination but remains an almost-everywhere identity, not a pointwise formula on null observations. | Read non-vacuity reviewCountable nonempty parameter spaces and finite Markov likelihoods instantiate the specialization without an authored domination proof; observations in a predictive null set remain intentionally unconstrained. | 2 / 0 / 1 |
|---|
fep-053Kernel Bayesian-Inversion Reconstruction | Bayesian Mechanics | Measure Bayesian Inversion | Formalized | fep053_kernelBayes_joint_reconstruction | Read invariantBayesian inversion reconstructs the swapped prior-likelihood joint measure, and at every positive finite evidence atom posterior mass times evidence equals the corresponding joint atom. | Read assumptionsThe measure theorem requires a finite prior and likelihood on a nonempty standard-Borel parameter space. The finite atom theorem additionally exposes strictly positive predictive evidence; it makes no normalized posterior claim at a zero-evidence atom. | Read non-vacuity reviewAny informative finite likelihood with a positive predictive atom exercises the atom reconstruction, while the measure equality covers the complete swapped joint rather than only one selected observation. | 2 / 0 / 1 |
|---|
fep-054Bayes Involution for Finite Joint Laws | Bayesian Mechanics | Measure Bayesian Inversion | Conditional Proxy | fep054_bayes_involution | Read invariantInverting a finite Markov likelihood twice returns the original likelihood prior-almost-everywhere, and one inversion followed by prediction reconstructs the prior exactly as a measure. | Read assumptionsThe likelihood and prior are native finite kernels and measures, not only finite atom tables. Involution requires both parameter and observation carriers to be nonempty standard Borel and the likelihood to be Markov; its conclusion is almost-everywhere rather than pointwise kernel equality. | Read non-vacuity reviewEvery finite Markov likelihood on nonempty standard-Borel spaces satisfies exact prior reconstruction, while distinct versions of a posterior on null observations explain why involution is stated almost everywhere. | 2 / 0 / 1 |
|---|
fep-055Composite-Kernel Bayesian Inversion | Bayesian Mechanics | Measure Bayesian Inversion | Conditional Proxy | fep055_compositeKernel_bayesInversion | Read invariantBayesian inversion reverses a two-kernel composition into the corresponding composition of inversions, and the associated predictive law is exactly the chronological two-stage prediction. | Read assumptionsThe prior and both kernels are finite, and the parameter and intermediate spaces are nonempty standard Borel. The inverse-kernel equality holds only almost everywhere under the final predictive law; predictive associativity itself is an unconditional measure equality under finiteness. | Read non-vacuity reviewTwo nonidentity finite kernels produce a genuine intermediate marginal and final predictive law, while final-predictive null observations retain the expected version ambiguity. | 2 / 0 / 1 |
|---|
fep-056Standard-Borel Conditional-Kernel Reconstruction | Bayesian Mechanics | Measure Bayesian Inversion | Formalized | fep056_standardBorel_condKernel_reconstruction | Read invariantMathlib's canonical conditional kernel reconstructs a finite joint measure from its first marginal and is normalized at every conditioning value. | Read assumptionsThe conditioned carrier must be nonempty standard Borel and the joint measure finite. This is the maintained standard-Borel disintegration theorem, not a claim that regular conditional probabilities exist on arbitrary measurable spaces. | Read non-vacuity reviewNonproduct finite joint measures are admitted, so reconstruction can retain genuine dependence; the Markov-kernel construction also specifies normalized values on marginal-null conditioning points. | 2 / 0 / 1 |
|---|
fep-057Conditional-Expectation Tower through a Kernel | Bayesian Mechanics | Measure Bayesian Inversion | Formalized | fep057_conditionalExpectation_tower | Read invariantIntegrating a conditional expectation against the conditioning marginal equals the original joint expectation, with a parallel extended-nonnegative tower law. | Read assumptionsThe joint measure is finite and the conditioned carrier nonempty standard Borel. Real-valued observables must be integrable; extended-nonnegative observables need measurability but no separate integrability premise. | Read non-vacuity reviewDependent finite joints and nonconstant observables exercise genuine nested integration, while nonintegrable signed observables are excluded rather than assigned a spurious finite expectation. | 2 / 0 / 1 |
|---|
fep-058Finite Gibbs Variational Principle | FEP | Variational Duality And Information Bounds | Formalized | fep058_gibbsVariational_lower_bound | Read invariantFinite Gibbs free energy is bounded below by minus the certified log partition, and the explicit normalized Gibbs law attains that bound. | Read assumptionsGibbsCertificate exposes strict support for reference and optimizer laws and the exact pointwise log-density identity. The theorem is finite and does not assert existence of such a certificate for arbitrary continuous potentials. | Read non-vacuity reviewOn every nonempty finite carrier, the uniform zero-potential certificate is full support and attains objective value zero, demonstrating compatible normalization and logarithmic assumptions. | 3 / 0 / 1 |
|---|
fep-059Finite Donsker–Varadhan Equality with a Full-Support Gibbs Optimizer | FEP | Variational Duality And Information Bounds | Formalized | fep059_donskerVaradhan_equality_iff | Read invariantThe finite Donsker–Varadhan objective is bounded by the certified log partition, with equality exactly at the supplied full-support Gibbs optimizer. | Read assumptionsThe result is parameterized by GibbsCertificate, whose strict-support and log-density fields make the finite logarithmic boundary explicit. It does not extend the equality to arbitrary measures, unbounded potentials, or an optimizer whose existence has not been certified. | Read non-vacuity reviewThe uniform zero-potential certificate from the shared foundation supplies a normalized full-support optimizer; unequal candidates have a strictly positive KL gap and therefore cannot attain equality. | 3 / 0 / 1 |
|---|
fep-060Coordinate ELBO Decomposition | FEP | Variational Duality And Information Bounds | Formalized | fep060_coordinateELBO_decomposition | Read invariantA finite joint ELBO separates exactly into a prior-coordinate score minus an expected conditional KL remainder, and that remainder is nonnegative. | Read assumptionsThe decomposition assumes every reference-prior and reference-kernel atom is strictly positive so all logarithmic rewrites are sound. Conditional KL nonnegativity is proved for the project's totalized finite divergence, but no zero-reference extended-real interpretation is claimed. | Read non-vacuity reviewDistinct actual and reference kernels yield a positive conditional remainder; matching kernels collapse only that coordinate penalty while leaving the prior-coordinate score visible. | 2 / 0 / 1 |
|---|
fep-061Mean-Field Coordinate Free-Energy Optimum | FEP | Variational Duality And Information Bounds | Formalized | fep061_meanFieldCoordinate_optimum_iff | Read invariantHolding one supported mean-field factor fixed reduces the coordinate free energy exactly to finite KL, whose unique zero is the supported target factor. | Read assumptionsThe fixed and target laws have full support on finite carriers. The theorem is a one-coordinate optimum with the other factor held fixed; it does not prove global convergence of alternating mean-field updates or handle continuous variational families. | Read non-vacuity reviewA candidate different from the full-support target has strictly positive coordinate free energy, whereas selecting the target attains the exact zero optimum for any full-support fixed factor. | 2 / 0 / 1 |
|---|
fep-062Fixed-Sample Importance-Weighted Jensen Bound | FEP | Variational Duality And Information Bounds | Formalized | fep062_iidProduct_importanceJensen | Read invariantFor a positive fixed sample count and positive weights, the IID product-law expectation of the log sample-mean weight is at most the log of its expected sample-mean weight. | Read assumptionsThe carrier is finite, NeZero excludes sample count zero, and every weight is strictly positive before Real.log is used. The positive-expectation witness additionally assumes a nonempty carrier and full-support sampling law. | Read non-vacuity reviewNonconstant positive importance weights on a nonempty finite carrier give a genuinely random positive sample mean; a one-sample law recovers the base finite Jensen inequality. | 3 / 0 / 1 |
|---|
fep-063Finite-Channel KL Data-Processing Inequality | FEP | Variational Duality And Information Bounds | Conditional Proxy | fep063_finiteChannel_klDataProcessing | Read invariantPassing two finite full-support laws through the same strictly positive finite channel cannot increase their finite KL divergence. | Read assumptionsInput is nonempty, both input laws have strict support, and every channel atom is strictly positive; these conditions force reference-predictive support and avoid the project's totalized-log boundary. This is stronger support than the most general measure-theoretic data-processing theorem. | Read non-vacuity reviewAny noisy positive channel acting on unequal full-support input laws exercises a genuine contraction comparison. Separate identity and complete-coarsening witnesses cover deterministic zero-entry channels: identity preserves finite KL and complete coarsening strictly reduces it for unequal laws. These do not weaken the support premises of the primary theorem or identify singular native infinity with the project's totalized finite convention. | 4 / 0 / 1 |
|---|
fep-064Rate–Distortion Lagrangian Weak Duality | FEP | Variational Duality And Information Bounds | Structural Proxy | fep064_rateDistortion_weakDuality | Read invariantSeparately certified lower bounds on finite mutual information and expected distortion combine into a lower bound on their rate–distortion Lagrangian for every nonnegative multiplier. Supporting theorems now additionally establish an attained information minimum for every nonempty finite fixed-source distortion-feasible set, an actual Lagrangian-infimum weak-duality bound, and an attained strictly positive optimum at fair Boolean Hamming budget one quarter. | Read assumptionsThe theorem assumes both component lower bounds rather than deriving a dual function. The supporting attainment theorem instead derives primal optimizer existence from compactness and the continuous zero-safe entropy expression for mutual information, requiring only a feasible finite joint with fixed source marginal. Infimum-derived weak duality requires nonnegative distortion and multiplier; zero-multiplier dual value requires a nonempty code alphabet. Neither general strong duality, dual attainment, a closed-form interior rate function, nor general optimizer uniqueness is claimed. The structural-proxy disposition and primary theorem remain unchanged: the primary theorem still assumes separately certified component lower bounds, while the independently reviewed supporting theorems establish finite optimizer attainment and infimum-derived weak duality. | Read non-vacuity reviewPositive multipliers make both certified components contribute, while setting the multiplier to zero reduces the Lagrangian exactly to mutual information and gives dual value zero. A concrete quarter-crossover Boolean joint makes the interior budget feasible, while every independent fair-source joint has distortion one half, forcing the attained quarter-budget optimum positive. Negative budgets are infeasible, zero budget forces a unique diagonal joint, and half budget has two distinct independent information minimizers. | 9 / 0 / 1 |
|---|
fep-065Controlled-Kernel Normalization | Active Inference | Control And Planning As Inference | Formalized | fep065_controlledKernel_normalization | Read invariantEvery action and source state in a finite controlled kernel selects a normalized next-state law. | Read assumptionsState and action carriers are finite and ControlledKernel is an action-indexed family of normalized FiniteKernel rows. No policy, controllability, stationarity, or infinite-horizon claim follows from row normalization alone. | Read non-vacuity reviewMultiple actions may select distinct nondegenerate transition rows while each retains unit mass, so the action index is not definitionally irrelevant. | 1 / 0 / 1 |
|---|
fep-066Action-Conditioned Bayesian Belief Update | Active Inference | Control And Planning As Inference | Formalized | fep066_actionConditioned_bayes_reconstruction | Read invariantA positive-evidence action-conditioned prediction and observation update is normalized and reconstructs its predicted state-observation joint mass. | Read assumptionsAll carriers are finite and the selected action has strictly positive observation evidence. The normalized posterior is not constructed at zero evidence, and the theorem concerns one update rather than policy optimality. | Read non-vacuity reviewInformative emissions after distinct action-conditioned transitions yield different posterior beliefs; the zero-evidence theorem pins the exact point where the normalized construction is unavailable. | 3 / 0 / 1 |
|---|
fep-067Reachable Finite-Belief POMDP Reduction | Active Inference | Control And Planning As Inference | Structural Proxy | fep067_reachableBelief_policyValue_equivalence | Read invariantExpanding a finite reachable-belief index into its interpreted finite law preserves every fixed finite-horizon feedback-policy value. | Read assumptionsReachableBeliefPOMDP supplies a finite indexed carrier, an interpretation into FiniteLaw, and sound positive-evidence updates; DecidableEq is required for the belief index. This is not a finite enumeration of the full probability simplex or an infinite-horizon POMDP reduction. | Read non-vacuity reviewThe concrete Boolean reachable model proves an exact positive-evidence Bayes update between two belief indexes, and arbitrary horizons exercise recursive policy-value preservation. | 2 / 0 / 1 |
|---|
fep-068Soft Bellman Recursion | Active Inference | Control And Planning As Inference | Formalized | fep068_softBellman_recursion | Read invariantOn a nonempty finite action carrier, a positive-temperature soft Bellman partition is positive, its successor value is the exact temperature-scaled log-sum-exp backup, and that soft value is no larger than any hard action energy. | Read assumptionsState and action sets are finite, the action carrier is inhabited, and temperature is strictly positive before division, logarithmic aggregation, and the soft-minimum comparison. The statement is an exact finite-horizon recursion and pointwise hard/soft bound, not an infinite-horizon fixed-point or optimality-limit theorem. | Read non-vacuity reviewInhabited actions make the exponential partition strictly positive; nonconstant costs and action-dependent transition rows make multiple exponentiated action values contribute to the finite soft minimum. | 1 / 0 / 1 |
|---|
fep-069KL-Control Desirability Recursion | Active Inference | Control And Planning As Inference | Structural Proxy | fep069_desirability_recursion | Read invariantOne finite desirability backup is an exponential state-cost tilt of a passive transition prediction and preserves nonnegativity. | Read assumptionsThe theorem gives the algebraic KL-control desirability operator on a finite Markov kernel. It does not derive this operator from a path-space KL objective, prove an optimal controlled kernel, or establish convergence of iteration. | Read non-vacuity reviewNonzero costs and nonconstant nonnegative desirability produce a nontrivial tilted prediction, while zero cost and unit desirability form an exact normalized fixed point. | 3 / 0 / 1 |
|---|
fep-070Control-as-Inference Policy Posterior | Active Inference | Control And Planning As Inference | Structural Proxy | fep070_controlPosterior_reconstruction | Read invariantA prior-weighted exponential action score normalizes to a control posterior whose mass reconstructs the unnormalized score. | Read assumptionsThe action carrier is finite, precision and costs are real, and positivity of the exponential partition is supplied by the finite Boltzmann construction. The result is an exact algebraic posterior but does not derive its cost from a full generative observation model. | Read non-vacuity reviewUnequal action costs and a supported prior reweight actions nonuniformly; identically zero costs return the prior exactly for every precision. | 3 / 0 / 1 |
|---|
fep-071Sophisticated Expected-Free-Energy Backward Induction | Active Inference | Control And Planning As Inference | Conditional Proxy | fep071_sophisticatedEFE_backward_step | Read invariantFinite sophisticated expected-free-energy recursion reoptimizes after each observation-dependent belief update, and a two-stage witness strictly separates feedback from every fixed open-loop second action. | Read assumptionsBelief, action, and observation carriers are finite and Action is nonempty so each finite argmin exists. The theorem is a maintained finite-horizon recursion with an exact Boolean two-stage witness; it does not prove continuous-state or infinite-horizon sophisticated planning. | Read non-vacuity reviewIn the witness, false and true observations choose different continuation actions, and the resulting expected cost is strictly below that of either fixed Boolean continuation. | 3 / 0 / 1 |
|---|
fep-072Hidden-Markov Forward Filtering Recursion | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep072_forward_filtering_recursion | Read invariantOne positive-evidence finite hidden-Markov filtering step reconstructs its predicted state-observation joint, with an exact asymmetric Boolean posterior witness. | Read assumptionsState and observation carriers are finite, transition and emission rows are normalized, and observed evidence is strictly positive. No filter is claimed at zero evidence and no continuous-state or Kalman–Bucy limit is inferred. | Read non-vacuity reviewThe asymmetric Boolean HMM assigns true posterior mass 20/23, while the zero-evidence theorem explicitly excludes an undefined normalization. | 3 / 0 / 1 |
|---|
fep-073Backward Information-Message Recursion | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep073_backward_message_recursion | Read invariantFinite backward information messages obey the exact future-observation recursion and preserve nonnegativity from one message to the preceding one. | Read assumptionsState and observation carriers are finite and transition and emission rows are normalized. Nonnegativity requires the supplied next message to be pointwise nonnegative; the theorem does not normalize messages or assert a limiting smoother. | Read non-vacuity reviewA nonempty future-observation list and nonconstant emission kernel produce a state-dependent backward message rather than only the terminal unit message. | 2 / 0 / 1 |
|---|
fep-074Forward–Backward Smoothing Factorization | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep074_forwardBackward_smoothing_factorization | Read invariantAt positive normalizer, a finite smoothing marginal factors into forward law times backward information, and one-step forward and backward computations agree on observation evidence. | Read assumptionsThe forward law is normalized, the backward message is nonnegative, and its weighted normalizer is strictly positive. The statement covers a finite factorization and does not assert positivity when all backward weights vanish. | Read non-vacuity reviewNonconstant backward messages reweight a nondegenerate forward law, while the evidence-agreement theorem connects independently expressed forward and backward one-step calculations. | 2 / 0 / 1 |
|---|
fep-075Smoothing-Marginal Normalization | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep075_smoothing_marginal_normalization | Read invariantA nonnegative forward–backward product with positive normalizer defines a normalized finite smoothing marginal. | Read assumptionsThe state carrier is finite, backward weights are pointwise nonnegative, and their forward expectation is strictly positive. The construction explicitly excludes a zero normalizer rather than selecting an arbitrary fallback law. | Read non-vacuity reviewThe Boolean smoother has unequal positive masses 7/46 and 39/46 whose sum is one; an identically zero backward message witnesses the excluded normalizer boundary. | 3 / 0 / 1 |
|---|
fep-076One-Step Normalized Variational State Update | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep076_variational_state_update_normalized | Read invariantA finite prior-weighted exponential energy tilt is normalized and reconstructs its unnormalized weight, with zero energy acting as the identity update. | Read assumptionsThe state carrier is finite and the real exponential makes the partition positive without a separate support premise. This is one exact normalized update, not convergence of a variational optimization algorithm. | Read non-vacuity reviewNonconstant energies reweight any prior with supported alternatives, whereas the zero-energy boundary leaves every prior law unchanged. | 3 / 0 / 1 |
|---|
fep-077Two-Level Hierarchical Predictive Factorization | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep077_hierarchical_predictive_factorization | Read invariantTwo-level finite hierarchical prediction is exactly prediction through the chronological composition of its two normalized kernels. | Read assumptionsUpper, middle, and observation carriers are finite and both conditional maps are FiniteKernel values. The result establishes two-level factorization only, not identifiability of latent levels or an unbounded hierarchy. | Read non-vacuity reviewNonidentity upper and lower kernels with a nondegenerate top law produce a predictive mixture that genuinely sums over the intermediate level. | 1 / 0 / 1 |
|---|
fep-078Bayesian Model-Averaging Predictive Law | Bayesian Mechanics | Temporal And Hierarchical Inference | Formalized | fep078_modelAverage_predictive_law | Read invariantBayesian model averaging is the prior-weighted finite mixture of model predictive laws and remains normalized. | Read assumptionsModel and observation sets are finite, the model prior is normalized, and each model predictive row is normalized. No posterior model update, asymptotic selection, or continuous model class is claimed. | Read non-vacuity reviewA nonuniform Boolean model prior and informative predictive kernel give the exact nontrivial true mass 13/20 while the complete mixture still sums to one. | 3 / 0 / 1 |
|---|
fep-079Blanket Factorization and Conditional-Mutual-Information Equivalence | Bayesian Mechanics | Causal Blankets And Interventions | Conditional Proxy | fep079_blanketFactorization_iff_conditionalMutualInformation_zero | Read invariantOn a finite conditional-blanket carrier with full blanket support, vanishing conditional mutual information is equivalent to pointwise internal–external factorization. | Read assumptionsBlanket, internal, and external carriers are finite and every blanket atom is strictly positive for the equivalence. The static-model specialization proves zero conditional mutual information even with null blanket atoms, but the theorem does not identify a general physical Markov blanket. | Read non-vacuity reviewStatic finite blanket models instantiate exact conditional product rows, and the full-support premise ensures that no nonfactorizing row is hidden behind a zero blanket probability. | 2 / 0 / 1 |
|---|
fep-080Shared-Conditional Mixture Preservation | Bayesian Mechanics | Causal Blankets And Interventions | Formalized | fep080_sharedConditional_mixture_preservation | Read invariantConvex mixing of two finite input laws commutes exactly with forming their joint laws when both components share the same conditional kernel. | Read assumptionsInput and output carriers are finite, the mixing weight lies in the closed unit interval, and both components use one identical normalized kernel. The result does not cover mixtures whose conditional mechanisms differ. | Read non-vacuity reviewThe half-mixture witness assigns mass one half to each Boolean atom, and distinct component laws may still produce a genuinely mixed joint after the shared kernel is applied. | 2 / 0 / 1 |
|---|
fep-081Coupled-Subsystem Blanket Composition | Bayesian Mechanics | Causal Blankets And Interventions | Structural Proxy | fep081_coupledSubsystem_blanketComposition | Read invariantTwo conditionally factorized subsystems retain zero paired-row mutual information under an arbitrarily coupled joint blanket law. | Read assumptionsEvery carrier is finite and subsystem internal and external kernels factor by their own blanket coordinates. The conclusion is rowwise conditional mutual information for paired variables; it does not assert that the joint blanket factorizes or that the complete subsystems are marginally independent. | Read non-vacuity reviewA diagonal Boolean blanket law has zero cross mass and strictly positive blanket mutual information, demonstrating genuine coupling despite exact within-row conditional factorization. | 2 / 0 / 1 |
|---|
fep-082Finite Intervention-Kernel Normalization | Bayesian Mechanics | Causal Blankets And Interventions | Formalized | fep082_interventionKernel_normalization | Read invariantA hard finite intervention kernel places unit mass on the chosen value, zero mass on every distinct value, and remains normalized in every context. | Read assumptionsContext and value carriers are finite and value equality is decidable. The kernel represents a deterministic do-assignment only; it does not by itself encode graph surgery, confounding assumptions, or interventional identifiability. | Read non-vacuity reviewOn any value carrier with two distinct elements, one receives mass one and the other mass zero independently of context, exercising both sides of the hard intervention. | 3 / 0 / 1 |
|---|
fep-083Non-Descendant Intervention Invariance | Bayesian Mechanics | Causal Blankets And Interventions | Conditional Proxy | fep083_nonDescendant_intervention_invariance | Read invariantIntervening on the root of the maintained ordered four-node model preserves the named non-descendant marginal while permitting a descendant marginal to change. | Read assumptionsThe result is scoped to OrderedFourNodeModel with finite carriers and a decidable root; the non-descendant is structurally assigned an independent root law. It does not prove intervention invariance for arbitrary DAGs or derive the graph from observational conditional independences. | Read non-vacuity reviewIn the Boolean witness, changing the root intervention moves the mediator's true mass from zero to one while the non-descendant marginal remains exactly unchanged. | 2 / 0 / 1 |
|---|
fep-084Ordered Finite Causal Factorization | Bayesian Mechanics | Causal Blankets And Interventions | Formalized | fep084_orderedFiniteCausal_factorization | Read invariantThe maintained four-node observational law is exactly its ordered product of two root laws and two parent-conditioned kernels, and that product normalizes. | Read assumptionsRoot, non-descendant, mediator, and outcome carriers are finite and every component is a normalized finite law or kernel. The carrier records one fixed parent order rather than a general acyclic-graph factorization calculus. | Read non-vacuity reviewNondegenerate root laws and nonconstant mediator and outcome kernels yield a dependent joint whose normalization requires summing every ordered factor. | 2 / 0 / 1 |
|---|
fep-085Local Markov Property from Ordered Factorization | Bayesian Mechanics | Causal Blankets And Interventions | Conditional Proxy | fep085_localMarkov_factorization_from_ordered | Read invariantIn the ordered four-node carrier, conditioning on the outcome's two parents factorizes the outcome from its non-parent predecessor root and forces their finite mutual information to zero. | Read assumptionsAll carriers are finite and mediator evidence must be strictly positive. The result is a local statement for one authored ordering and parent set; it is not a proof of general d-separation, faithfulness, or native measurable conditional independence. | Read non-vacuity reviewThe Boolean model conditions on a mediator event of positive half mass and obtains zero mutual information, while a separate theorem marks zero mediator evidence as outside the conditional construction. | 4 / 0 / 1 |
|---|
fep-086Precision-Weighted Prediction-Error Energy | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep086_precisionWeighted_zero_iff_exactPrediction | Read invariantNonnegative precision yields nonnegative scalar prediction-error energy, and under positive precision zero energy occurs exactly at exact prediction. | Read assumptionsThe carrier is scalar real arithmetic. Nonnegativity needs precision at least zero and separation needs precision strictly positive; zero precision cannot distinguish any estimate from the observation. | Read non-vacuity reviewObservation one, estimate zero, and precision two have exact unit energy, so the energy and its separating zero condition are not vacuous. | 3 / 0 / 1 |
|---|
fep-087Hierarchical Predictive-Coding Energy Decomposition | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep087_hierarchicalPredictiveCoding_decomposition | Read invariantFinite hierarchical predictive-coding energy decomposes into the zeroth precision-weighted error plus all successor-level errors and is nonnegative when every precision is nonnegative. | Read assumptionsThe hierarchy is finite and energies are explicit scalar quadratics. Nonnegativity requires pointwise nonnegative precision; the result does not model neural implementation, learned precision, or an infinite hierarchy. | Read non-vacuity reviewA concrete two-level hierarchy has both levels contribute and evaluates to eleven, ruling out a decomposition that silently drops the upper level. | 3 / 0 / 1 |
|---|
fep-088Prediction-Error Gradient Identity | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep088_predictionError_gradient_identity | Read invariantDifferentiating scalar precision-weighted prediction-error energy with respect to the estimate gives exactly minus precision times signed prediction error. | Read assumptionsThe theorem is an exact HasDerivAt statement for a scalar quadratic and requires no positivity assumption for differentiation. It does not assert a gradient for a nonlinear decoder, a vector network, or a stochastic process. | Read non-vacuity reviewAt precision two, observation one, and estimate zero, the named gradient is exactly minus two and therefore drives a nontrivial correction. | 3 / 0 / 1 |
|---|
fep-089Finite Generalized-Coordinate Shift Semigroup | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep089_finiteJet_shift_semigroup | Read invariantNatural-number shifts on a finite generalized-coordinate jet compose associatively, with the highest retained coordinate shifting into an explicit zero truncation boundary. | Read assumptionsGeneralized coordinates are finite jets represented by finitely supported coefficients. The semigroup is discrete and exact; no analytic infinite jet, time derivative, or continuous-flow convergence is claimed. | Read non-vacuity reviewA first-order jet moves velocity into the position coordinate while its terminal velocity coordinate becomes zero, visibly exercising the truncation. | 3 / 0 / 1 |
|---|
fep-090Finite-Jet Generalized-Filtering Correction Equation | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep090_finiteJet_generalizedFiltering_correctionEquation | Read invariantOne finite-jet generalized-filtering Euler step equals the current coordinate plus a truncated shift minus the certified quadratic energy gradient. | Read assumptionsStep size and coordinate precisions are real and the jet order is finite. The pointwise correction has an exact scalar derivative witness, but the theorem does not identify an infinite generalized flow or prove stability of repeated coupled-jet updates. | Read non-vacuity reviewA concrete first-order half-step gives exact nonzero corrections 3/2 and 1/2 at the two retained coordinates, while the top-coordinate theorem removes the truncated shift term. | 4 / 0 / 1 |
|---|
fep-091Precision Modulation of Prediction Error | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep091_precisionModulation_energy_mono | Read invariantIncreasing nonnegative precision cannot decrease a fixed scalar prediction-error energy, and scaling precision scales its exact gradient by the same factor. | Read assumptionsEnergy monotonicity assumes a nonnegative lower precision and an ordered upper precision. Gradient scaling is algebraic for arbitrary real scale, including negative values, but only nonnegative precision retains an energy weighting interpretation. | Read non-vacuity reviewDoubling precision from one to two at a unit prediction error exactly doubles the energy and makes the inequality strict. | 3 / 0 / 1 |
|---|
fep-092Quadratic Predictive-Coding Convergence | FEP | Predictive Coding And Generalized Coordinates | Formalized | fep092_quadraticPredictiveCoding_error_tendsto_zero | Read invariantExact scalar quadratic prediction updates contract energy by the squared factor one minus step size, strictly decrease positive-precision nonzero error for step sizes in the open interval zero to two, and drive error to zero. | Read assumptionsConvergence requires 0 < stepSize < 2; strict descent additionally requires positive precision and unequal target and estimate. The result is scalar and exact-quadratic, not a convergence theorem for nonlinear predictive-coding networks. | Read non-vacuity reviewAt precision two and half-step size, a unit error has energy one, moves to estimate one half, and drops to energy one quarter. | 4 / 0 / 1 |
|---|
fep-093Forward and Reverse Finite Path-Law Ratio | Thermodynamics | Path Space Stochastic Thermodynamics | Formalized | fep093_forward_reverse_pathLaw_ratio | Read invariantA finite forward path law is reconstructed pointwise from its supported reverse-aligned law and likelihood ratio, while both path laws normalize and path reversal is involutive. | Read assumptionsThe path carrier is finite and reverse-aligned mass must be strictly positive for the ratio reconstruction. FinitePathProtocol stores normalized laws and an involution; it does not derive reversal or reverse dynamics from a microscopic process. | Read non-vacuity reviewUnequal full-support forward and reverse-aligned laws yield nonunit path ratios, while an involution with a two-path swap exercises a genuine reversal. | 3 / 0 / 1 |
|---|
fep-094Entropy Production as Path KL | Thermodynamics | Path Space Stochastic Thermodynamics | Structural Proxy | fep094_entropyProduction_as_pathKL | Read invariantMean finite path entropy production is the KL divergence from the forward to reverse-aligned path law, is nonnegative, and under full support equals the forward expectation of the pointwise log ratio. | Read assumptionsThe primary equality is the maintained definition of entropyProduction. Expected-log-ratio expansion requires strict support of both path laws, and the project's totalized real KL is not an extended divergence at zero reverse mass. | Read non-vacuity reviewThe compiled irreversible Boolean protocol has unequal full-support path laws and therefore supplies positive, rather than merely nonnegative, production in the later dissipation topic. | 3 / 0 / 1 |
|---|
fep-095Detailed Fluctuation Symmetry | Thermodynamics | Path Space Stochastic Thermodynamics | Conditional Proxy | fep095_detailedFluctuation_symmetry | Read invariantUnder full path support, reverse-aligned mass times exponential pointwise entropy production reconstructs forward mass, and an exchanging reversal makes entropy production antisymmetric. | Read assumptionsForward and reverse-aligned laws are strictly positive. Antisymmetry further assumes that the recorded involution exchanges the two aligned laws in both directions; these exchange laws are not derived from protocol dynamics. | Read non-vacuity reviewA two-path protocol with swapped unequal full-support masses has nonzero pointwise entropy production whose sign reverses on the paired path. | 2 / 0 / 1 |
|---|
fep-096Integral Fluctuation Theorem | Thermodynamics | Path Space Stochastic Thermodynamics | Formalized | fep096_integralFluctuation_theorem | Read invariantThe forward expectation of exponential negative pointwise entropy production equals one for normalized finite full-support forward and reverse path laws. | Read assumptionsThe path carrier is finite and both path laws have strict support, so the likelihood ratio and logarithm are ordinary real values. The theorem does not treat singular path measures or continuous-time trajectories. | Read non-vacuity reviewUnequal full-support path laws produce nonconstant entropy-production values whose weighted exponentials still normalize exactly to one. | 1 / 0 / 1 |
|---|
fep-097Finite Jarzynski Equality | Thermodynamics | Path Space Stochastic Thermodynamics | Conditional Proxy | fep097_finiteJarzynski_equality | Read invariantA normalized finite exponential-work protocol has work average equal to the exponential of negative inverse temperature times free-energy difference. | Read assumptionsHasJarzynskiNormalization explicitly packages positive beta and the identity that the expectation of exp(-beta times (work minus free-energy difference)) equals one. The theorem algebraically extracts Jarzynski's equality from this normalization; it does not derive that premise from microscopic reversibility. | Read non-vacuity reviewNonconstant finite work values can satisfy the normalization after choosing a compatible free-energy difference, while beta positivity excludes the zero-temperature-parameter collapse. | 1 / 0 / 1 |
|---|
fep-098Local Detailed Balance and Current Cancellation | Thermodynamics | Path Space Stochastic Thermodynamics | Formalized | fep098_localDetailedBalance_currentCancellation | Read invariantDetailed balance cancels every oriented finite probability current, while a zero reverse rate is exposed as a totalized-log affinity boundary. | Read assumptionsThe law and transition kernel are normalized finite carriers and current cancellation assumes IsReversible. The zero-rate theorem reports the project's real-log value zero and must not be read as a finite extended-real affinity. | Read non-vacuity reviewSymmetric positive bidirectional transitions give exact zero current under a reversible law, whereas a one-way edge exercises the separately labeled zero-reverse-rate boundary. | 2 / 0 / 1 |
|---|
fep-099Reversible-Chain One-Step KL Dissipation | Thermodynamics | Path Space Stochastic Thermodynamics | Formalized | fep099_reversibleChain_oneStep_KL_dissipation | Read invariantOne strictly positive reversible finite Markov step cannot increase KL to its stationary law; the identity transition saturates equality and an explicit irreversible path protocol has positive entropy production. | Read assumptionsState is finite and nonempty, actual and stationary laws have full support, every transition atom is positive, and detailed balance supplies stationarity. The result is one-step dissipation, not strict contraction for every nonidentity kernel or a continuous-time entropy-production theorem. | Read non-vacuity reviewThe identity kernel proves the exact reversible equality boundary, while the unequal full-support Boolean path witness proves strictly positive production away from reversibility. | 3 / 0 / 1 |
|---|
fep-100Categorical Fisher Positivity on Simplex Tangents | Info Geometry | Information Geometry And Geometric Optimization | Conditional Proxy | fep100_categoricalFisher_simplexTangent_positivity | Read invariantThe inherited Fisher metric is strictly positive on every certified nonzero categorical simplex tangent under full support, while a duplicated-score model exhibits an explicit nonzero null direction. | Read assumptionsCategoricalFisherCarrier packages a full-support law, an existing ScoreModel, and exact metric and lowering-map representations on simplex tangents. The general positivity theorem depends on this certificate. A separate genuine Fin 2 categorical construction proves that its one-dimensional simplex tangent space is spanned by (1,-1) and is positive definite there; no claim is made that every arbitrary score parameterization is full rank. | Read non-vacuity reviewThe explicit Fin 2 categorical law and nonzero tangent (1,-1) have Fisher energy exactly four, and every Fin 2 simplex tangent is a multiple of that direction. Duplicated score coordinates separately give a nonzero tangent with zero Fisher energy. | 5 / 0 / 1 |
|---|
fep-101Fisher Pullback under Reparameterization | Info Geometry | Information Geometry And Geometric Optimization | Formalized | fep101_fisherPullback_reparameterization | Read invariantPulling the existing finite Fisher metric through a composite Jacobian equals successive pullback, and every such pullback is positive semidefinite. | Read assumptionsOutcome and coordinate carriers are finite and Jacobians are finite real matrices. No invertibility is needed for pullback or semidefiniteness, so a rank-deficient chart may retain null directions; positive definiteness is not claimed here. | Read non-vacuity reviewNonidentity rectangular Jacobians exercise genuine reparameterization, while a rank-deficient matrix demonstrates why the conclusion is nonnegative rather than strictly positive. | 2 / 0 / 1 |
|---|
fep-102Unbiased Scalar Cramér–Rao Bound under Score Regularity | Info Geometry | Information Geometry And Geometric Optimization | Formalized | fep102_unbiasedScalar_cramerRao | Read invariantFinite unbiased scalar estimation under score regularity and positive Fisher information satisfies variance times Fisher information at least one. | Read assumptionsScalarCramerRaoCertificate explicitly records centered unbiasedness, unit estimator–score covariance, and strictly positive scalar Fisher information for an existing one-parameter ScoreModel. The theorem does not derive score regularity by differentiating a parameterized family or cover biased estimators. | Read non-vacuity reviewPositive Fisher information rules out an identically zero score, and unit score covariance rules out a constant centered estimator, so the Cauchy–Schwarz bound cannot be discharged by a degenerate zero product. | 1 / 0 / 1 |
|---|
fep-103Natural-Gradient Equivariance under an Invertible Full-Rank Chart | Info Geometry | Information Geometry And Geometric Optimization | Formalized | fep103_naturalGradient_equivariance | Read invariantUnder invertible Fisher and chart matrices, the natural gradient transports equivariantly so lowering the chart-coordinate vector yields the pulled-back covector. | Read assumptionsThe finite ScoreModel Fisher matrix and square chart Jacobian each carry an Invertible instance. Rank-deficient metrics or charts are excluded because the natural-gradient and chart-coordinate inverses would not be uniquely defined. The supporting weighted Cauchy–Schwarz theorem requires positive right energy. | Read non-vacuity reviewNonidentity invertible charts change vector coordinates while preserving the lowered covector law; the proof spike also excludes a zero-energy right vector before deriving its finite weighted inequality. | 2 / 0 / 1 |
|---|
fep-104Mirror-Descent Three-Point Identity | Info Geometry | Information Geometry And Geometric Optimization | Formalized | fep104_mirrorDescent_threePoint_identity | Read invariantThe algebraic Bregman expression associated with supplied potential and gradient data obeys the exact three-point identity used by mirror descent. | Read assumptionsThe coordinate carrier is finite and potential and gradient are arbitrary supplied functions. The identity is algebraic and assumes neither convexity nor that the gradient is the derivative of the potential; those extra properties are required before interpreting every term as a nonnegative divergence or an algorithmic descent guarantee. | Read non-vacuity reviewDistinct left, middle, and right vectors with a nonconstant supplied gradient give nonzero pairing and divergence differences while retaining exact equality. | 1 / 0 / 1 |
|---|
fep-105Bregman Pythagorean Law for an Affine Information Projection | Info Geometry | Information Geometry And Geometric Optimization | Conditional Proxy | fep105_affineProjection_bregmanPythagorean | Read invariantAn affine projection certificate yields exact Bregman Pythagorean splitting, and a nonnegative residual divergence makes the certified projection a minimizer over the maintained affine set. | Read assumptionsAffineBregmanProjection explicitly supplies projection membership and gradient-difference orthogonality for every candidate. Minimization separately assumes residual Bregman nonnegativity. Existence, uniqueness, convexity, and differentiability of the projection are not derived. | Read non-vacuity reviewCandidates distinct from the projection can have a positive residual term, producing a strict objective gap; zero residual gives the exact equality boundary without proving uniqueness. | 2 / 0 / 1 |
|---|
fep-106Replicator–Natural-Gradient Equivalence | Info Geometry | Information Geometry And Geometric Optimization | Conditional Proxy | fep106_replicator_naturalGradient_equivalence | Read invariantOn a certified categorical Fisher carrier, the replicator vector is the natural gradient of centered fitness and has zero total mass. | Read assumptionsCategoricalFisherCarrier supplies full support and the exact bridge from the existing ScoreModel lowering map to categorical coordinates. The result is an instantaneous finite-simplex vector-field identity, not positivity preservation or convergence of a time-integrated replicator flow. | Read non-vacuity reviewThe explicit full-support Fin 2 categorical law with nonconstant fitness yields a nonzero mass-conserving replicator vector and satisfies the inherited natural-gradient predicate; constant fitness produces the exact zero field boundary. | 3 / 0 / 1 |
|---|
fep-107Product-Agent Generative Law | Active Inference | Collective And Multiagent Active Inference | Formalized | fep107_productAgent_generative_mass | Read invariantIndependent product priors and product observation kernels yield a normalized joint kernel whose generative mass factors exactly into the two agent-level generative masses. | Read assumptionsBoth state and observation carriers are finite and each component law and kernel is normalized. Independence is built into FiniteLaw.product and the productKernel coordinate definition; the theorem does not infer independence from an arbitrary coupled multiagent law. | Read non-vacuity reviewNondegenerate component priors and nonconstant component kernels make all four coordinates contribute to joint mass while product-kernel normalization still requires summing over every paired observation. | 2 / 0 / 1 |
|---|
fep-108Additive Collective Variational Free Energy | Active Inference | Collective And Multiagent Active Inference | Formalized | fep108_collectiveVFE_additive | Read invariantVariational free energy of independent product laws with additive cost is exactly the sum of the two agent-level free energies. | Read assumptionsState carriers are finite, both reference factors have full support, actual and reference joint laws are products, and joint cost is additive. The result does not discard a dependence or interaction term for a coupled law or nonadditive cost. | Read non-vacuity reviewUnequal actual and reference factors with nonconstant component costs make both KL and expectation terms contribute, while the separate product-cost theorem isolates the expectation part of additivity. | 2 / 0 / 1 |
|---|
fep-109Independent-Agent Expected-Free-Energy Additivity | Active Inference | Collective And Multiagent Active Inference | Formalized | fep109_independentEFE_additive | Read invariantExpected free energy of product predictive and preference laws with additive ambiguity equals the sum of independent agent-level expected free energies. | Read assumptionsBoth finite preference factors have full support, predictive and preference joint laws are products, and ambiguity is coordinate-additive. No additivity is claimed for statistically coupled agents, shared outcomes, or a nonseparable ambiguity functional. | Read non-vacuity reviewDistinct predictive and preference factors yield nonzero risk terms, while nonconstant ambiguity functions make both component expectations contribute to the collective value. | 2 / 0 / 1 |
|---|
fep-110Unit-Weight Product-of-Experts Pool Normalization | Active Inference | Collective And Multiagent Active Inference | Formalized | fep110_unitWeightProductOfExpertsPool_normalized | Read invariantThe unit-weight finite product-of-experts pool is the normalized pointwise product of two laws and has total mass one whenever its normalizer is positive. | Read assumptionsThe state carrier is finite and the pointwise-product normalizer must be strictly positive. Disjoint supports are excluded. This unit-weight product uses exponents one, not the one-half exponents of an equal-weight logarithmic pool, and no externally Bayesian pooling property is claimed. | Read non-vacuity reviewTwo distinct overlapping laws produce a pooled distribution different from either input; the positive-overlap premise visibly excludes the disjoint point mass boundary. | 2 / 0 / 1 |
|---|
fep-111Consensus Mass Conservation | Active Inference | Collective And Multiagent Active Inference | Formalized | fep111_consensus_pointwise_mass_conserved | Read invariantThe specified doubly stochastic two-agent consensus update conserves combined mass at every state and therefore preserves total combined mass two. | Read assumptionsThe state carrier is finite and both inputs are normalized FiniteLaw values. Conservation is for the maintained two-agent mixing operator; it does not establish consensus, stationarity, or conservation for arbitrary interaction matrices. | Read non-vacuity reviewUnequal input laws redistribute statewise mass between agents while the exact pointwise sum remains fixed and the two output laws each remain normalized. | 2 / 0 / 1 |
|---|
fep-112Contractive Belief-Consensus Convergence | Active Inference | Collective And Multiagent Active Inference | Formalized | fep112_consensus_converges | Read invariantIterating the maintained strictly stochastic two-agent update halves each atomwise belief gap and drives pointwise disagreement to zero. | Read assumptionsState is finite and consensus uses the fixed one-quarter/three-quarter mixing matrix encoded by consensusLeft and consensusRight. Convergence is pointwise for two agents; no arbitrary network topology, time-varying weights, or rate in a global probability metric is claimed. | Read non-vacuity reviewOpposite Boolean point masses begin with unit gap, retain positive gap one half after one update, and satisfy a strict decrease rather than a zero-gap tautology. | 3 / 0 / 1 |
|---|
fep-113Coupled-Agent Potential Descent | Active Inference | Collective And Multiagent Active Inference | Formalized | fep113_coupledPotential_strict_descent | Read invariantThe maintained consensus coupling quarters atomwise quadratic disagreement potential and decreases it strictly whenever the two input masses differ at that atom. | Read assumptionsState is finite and the potential is the exact scalar square of the two-agent atomwise gap under the fixed consensus operator. Strictness requires explicit separation; the theorem does not cover a general coupled free-energy functional or nonlinear multiagent dynamics. | Read non-vacuity reviewAny state at which the two laws assign unequal mass has positive initial potential and a strictly smaller positive quarter-potential after one update. | 2 / 0 / 1 |
|---|
fep-114Sub-Gaussian Empirical-Mean Tail Bound | FEP | Learning Concentration And Model Evidence | Formalized | fep114_subGaussian_empiricalMean_tail | Read invariantA finite independent family with certified sub-Gaussian moment-generating functions satisfies the explicit exponential upper-tail bound for its summed empirical-mean event. | Read assumptionsObservables are indexed by Fin sampleCount, are independent under the supplied measure, and each has a nonnegative sub-Gaussian proxy variance. Deviation is nonnegative. The theorem neither assumes IID data nor asserts an asymptotic law; a positive sample count is needed for the usual empirical-mean interpretation even though real division is totalized at zero. | Read non-vacuity reviewMultiple independent nonconstant centered observables with positive proxy variances give a nontrivial exponentially decaying bound as deviation grows. | 2 / 0 / 1 |
|---|
fep-115Simultaneous Finite-Alphabet Frequency Bound | FEP | Learning Concentration And Model Evidence | Formalized | fep115_simultaneous_frequency_bound | Read invariantPer-symbol empirical-frequency failure bounds combine by a finite union bound into an alphabet-wide failure probability bounded by alphabet size times the per-symbol rate. | Read assumptionsThe sampling measure is a probability measure, the alphabet is finite with decidable equality, sample count is nonzero, and every symbol has the supplied probability bound. No independence or concentration rate is inferred beyond those per-symbol premises. | Read non-vacuity reviewA multi-symbol alphabet and positive sample count make the union contain genuinely distinct two-sided normalized-count deviation events. | 2 / 0 / 1 |
|---|
fep-116Finite-Hypothesis PAC-Bayes Loss-Gap Bound | FEP | Learning Concentration And Model Evidence | Formalized | fep116_finitePACBayes_with_confidence | Read invariantFor any finite posterior, a Gibbs certificate whose potential is inverse temperature times the population-minus-empirical loss gap converts a certified log-MGF budget into an empirical-loss plus KL-complexity population-loss bound. | Read assumptionsHypotheses are finite; inverse temperature is positive; the Gibbs reference equals the prior and carries full support; confidence lies in (0,1); and the certificate log partition is bounded by log(confidence^-1). The theorem is deterministic conditional on this log-MGF premise and does not itself prove that the premise holds with high probability over data. | Read non-vacuity reviewUnequal posterior and prior laws contribute a finite KL penalty, nonzero loss gaps enter through the certified potential, and smaller confidence increases the explicit log(confidence^-1) budget. | 2 / 0 / 1 |
|---|
fep-117Posterior-Odds Multiplicative Recursion | FEP | Learning Concentration And Model Evidence | Formalized | fep117_posteriorOdds_recursion | Read invariantAt positive evidence, posterior odds equal prior odds times the likelihood ratio, and a zero-prior hypothesis retains zero posterior mass. | Read assumptionsHypothesis and evidence carriers are finite. Total evidence, the reference prior mass, and the reference likelihood must be strictly positive before forming ordinary real odds. The zero-prior theorem marks lack of posterior support rather than permitting recovery by conditioning. | Read non-vacuity reviewUnequal positive likelihoods move the favored-to-reference odds multiplicatively, while a separate zero-prior hypothesis remains exactly absent from the posterior. | 2 / 0 / 1 |
|---|
fep-118Exponential Posterior Concentration from a Likelihood Gap | FEP | Learning Concentration And Model Evidence | Formalized | fep118_posteriorGap_concentration | Read invariantA nonnegative per-observation likelihood gap yields an explicit exponential finite-sample upper bound on inferior two-hypothesis posterior weight. | Read assumptionsGood prior and likelihood weights are strictly positive, bad weights and the gap are nonnegative, and bad likelihood is bounded by exp(-gap) times good likelihood. These are scalar two-hypothesis weights, not a theorem of consistency for an arbitrary normalized model class. | Read non-vacuity reviewEqual priors with likelihood ratio three to one give exact inferior posterior mass one tenth after two observations, so the posterior is positive yet genuinely concentrated. | 2 / 0 / 1 |
|---|
fep-119Bayesian-Mixture Log-Loss Regret Bound | FEP | Learning Concentration And Model Evidence | Formalized | fep119_mixtureLogLoss_regret | Read invariantFinite Bayesian-mixture evidence dominates every nonnegative component contribution, so mixture log loss is at most selected-component log loss plus its exact negative-log-prior penalty. | Read assumptionsHypotheses are finite, all component likelihood weights are nonnegative, and the selected prior and likelihood weights are strictly positive before logarithms are compared. No sequential regret sum, stochastic calibration, or asymptotic optimality is claimed. | Read non-vacuity reviewA positive selected component contributes strictly to mixture evidence, and a prior below one produces a positive finite complexity penalty rather than a vacuous zero term. | 2 / 0 / 1 |
|---|
fep-120Bayes-Factor Multiplicativity and Model-Evidence Update | FEP | Learning Concentration And Model Evidence | Formalized | fep120_bayesFactor_multiplicative_update | Read invariantExplicitly factorized evidence ratios multiply, and sequential model-odds updates equal one update using product evidence. | Read assumptionsBoth reference evidence factors must be nonzero for multiplicativity in the real field. Evidence factorization is supplied algebraically and does not establish probabilistic independence. At a zero denominator, totalized real division returns zero rather than an infinite Bayes factor. | Read non-vacuity reviewEvidence three quarters versus one quarter maps unit prior odds to three, and the separate zero-reference theorem pins the exact unsupported comparison boundary. | 3 / 0 / 1 |
|---|
fep-121Laplace-Smoothing Error Identity | FEP | Finite Sample Risk And Calibration | Formalized | fep121_laplaceError_identity | Read invariantFor a positive finite sample, add-one smoothing decomposes forecast error into contracted empirical error plus an exact target-dependent offset. | Read assumptionsThe success count and sample count are natural numbers, sample count is positive, successes do not exceed it, and the target lies in the unit interval. The theorem is an algebraic identity, not a stochastic consistency or posterior-contraction result. | Read non-vacuity reviewThe shrinkage coefficient lies in the unit interval and the separate boundary witness in fep-122 shows that the offset can be nonzero. | 2 / 0 / 1 |
|---|
fep-122Laplace-Smoothing Bias Bound | FEP | Finite Sample Risk And Calibration | Formalized | fep122_laplaceBias_abs_le | Read invariantThe absolute target-dependent Laplace offset is at most one pseudo-count divided by the smoothed sample size. | Read assumptionsThe target is confined to the closed unit interval. The bound controls the deterministic smoothing offset and does not identify statistical bias under an unspecified sampling distribution. | Read non-vacuity reviewAt sample count two and target zero, the offset equals one quarter and is explicitly nonzero. | 2 / 0 / 1 |
|---|
fep-123Absolute-Error Transfer through Laplace Smoothing | FEP | Finite Sample Risk And Calibration | Formalized | fep123_laplaceAbsoluteError_le | Read invariantAn absolute empirical-error certificate transfers through add-one smoothing with the exact shrinkage coefficient and one-pseudo-count offset. | Read assumptionsSample count is positive, successes are bounded by it, the target is in the unit interval, and the raw empirical error already has a supplied bound. No probability tail rate is inferred in this row. | Read non-vacuity reviewThe source error may be positive and the smoothing offset remains visible; the theorem also proves that any supplied error upper bound is nonnegative. | 2 / 0 / 1 |
|---|
fep-124Squared-Risk Transfer through Laplace Smoothing | FEP | Finite Sample Risk And Calibration | Formalized | fep124_laplaceSquaredError_le | Read invariantSquared add-one error is bounded pointwise by twice the contracted empirical squared error plus twice the squared pseudo-count offset, and the inequality integrates under every normalized finite sampling law. | Read assumptionsSample count is positive, each success count is bounded by it, and the target is in the unit interval. The factor-two inequality is conservative and finite-law expectation is not an asymptotic risk claim. | Read non-vacuity reviewNonzero empirical error and nonzero boundary offset both contribute to the integrated upper bound under a nondegenerate finite sampling law. | 2 / 0 / 1 |
|---|
fep-125Bernoulli Brier Excess-Risk Identity | FEP | Finite Sample Risk And Calibration | Formalized | fep125_brierExcess_eq_sqError | Read invariantBernoulli Brier excess risk relative to the true probability is exactly the squared forecast error. | Read assumptionsThe identity is polynomial and therefore holds over real target and forecast inputs; the probability interpretation requires both to lie in the unit interval, which is supplied by downstream statistical uses. | Read non-vacuity reviewA forecast unequal to the target has positive squared excess, while the self-forecast boundary has exactly zero excess. | 2 / 0 / 1 |
|---|
fep-126Finite-Law Laplace Brier-Risk Bound | FEP | Finite Sample Risk And Calibration | Formalized | fep126_laplaceBrierRisk_le | Read invariantFinite-law expected Brier excess for the add-one forecast inherits the squared-error transfer bound. | Read assumptionsSampling uses the normalized FiniteLaw carrier, sample count is positive, success counts are bounded, and the target is in the unit interval. This is an expected finite-model inequality, not an empirical performance report. | Read non-vacuity reviewA sampling law with mass on outcomes having unequal success counts produces a genuine weighted risk while retaining total mass one. | 2 / 0 / 1 |
|---|
fep-127Concentration-Event Transfer through Smoothing | FEP | Finite Sample Risk And Calibration | Formalized | fep127_laplaceBadEvent_subset | Read invariantA smoothed deviation beyond the transferred threshold is contained in the corresponding raw empirical-deviation event, so any supplied finite-law probability bound transfers monotonically. | Read assumptionsSample count is positive, success counts are bounded, the target is in the unit interval, and a raw event-probability bound is supplied. The theorem composes with concentration results but does not derive their assumptions or rates itself. | Read non-vacuity reviewThe smoothed and raw events are distinct whenever the shrinkage and offset change the threshold, and the finite-law monotonicity result applies to any nonzero failure bound. | 2 / 0 / 1 |
|---|
fep-128Observation-Contingent Policy-Tree Recursion | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep128_policyTreeValue_node | Read invariantA finite policy-tree node equals its stage cost plus the observation-law weighted values of observation-contingent continuation trees. | Read assumptionsBelief, action, and observation carriers are finite and the horizon is a natural-number depth. Observation laws and deterministic belief updates are supplied by the model; no infinite-horizon or continuous-belief claim is made. | Read non-vacuity reviewA successor node can choose different continuation trees after different observations, whereas the depth-zero carrier has exactly zero value. | 2 / 0 / 1 |
|---|
fep-129Finite Policy-Tree Bellman Minimum | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep129_optimalTreeValue_eq_min | Read invariantBackward induction exposes an exact finite-action Bellman minimum of stage cost plus observation-weighted optimal continuation. | Read assumptionsThe action carrier is finite and nonempty, and belief and observation carriers are finite. The result is one finite-horizon recursion, not a contraction or fixed-point theorem. | Read non-vacuity reviewThe selected action is proved no worse than every explicit alternative at each node rather than merely being named as an argmin. | 2 / 0 / 1 |
|---|
fep-130Optimal Finite Policy-Tree Existence | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep130_exists_optimalPolicyTree | Read invariantEvery finite-depth, finite-carrier policy-tree problem with a nonempty action set has a concrete backward-inducted tree attaining the recursive optimum. | Read assumptionsAll carriers and the horizon are finite and the action carrier is nonempty. Existence does not extend to unbounded horizon, arbitrary measurable policy spaces, or continuous beliefs. | Read non-vacuity reviewThe witness is an actual depth-indexed tree and is compared with every other tree on the same finite carrier. | 2 / 0 / 1 |
|---|
fep-131Open-Loop Plan Embedding into Policy Trees | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep131_openLoopEmbedding_value | Read invariantReusing the same continuation after every observation embeds an open-loop action plan into the policy-tree carrier without changing its recursive value. | Read assumptionsThe comparison uses the same model, belief, and finite depth. Open-loop plans ignore observations by construction; the theorem does not identify arbitrary state-feedback policies with open-loop sequences. | Read non-vacuity reviewAt positive depth the embedding duplicates a common continuation across all observation branches; at depth zero both carriers reduce to their unique leaf. | 2 / 0 / 1 |
|---|
fep-132Closed-Loop Policy-Tree Dominance over Open Loop | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep132_optimalTree_le_openLoop | Read invariantThe optimal observation-contingent finite policy tree is no worse than every open-loop plan embedded at the same depth. | Read assumptionsActions are finite and nonempty, all other carriers are finite, and both sides share one finite horizon and cost model. No infinite-horizon POMDP dominance is claimed. | Read non-vacuity reviewThe strict Boolean witness in fep-134 demonstrates that the inequality can be strict rather than only equality under an observation-irrelevant model. | 2 / 0 / 1 |
|---|
fep-133Treewise Expected-Free-Energy Decomposition | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep133_policyTree_efe_eq_risk_add_ambiguity | Read invariantThe one-step full-support expected-free-energy identity lifts through every branch of a finite policy tree, and the corresponding optimal values agree. | Read assumptionsEvery belief-indexed finite generative model satisfies the maintained FullSupport contract. Belief updates and horizons are finite; the theorem transports the existing risk-plus-ambiguity identity and does not establish its empirical adequacy. | Read non-vacuity reviewThe induction ranges over observation-contingent continuations and the optimal-value theorem compares independently constructed minimizing trees. | 2 / 0 / 1 |
|---|
fep-134Strict Boolean Feedback Advantage | Active Inference | Closed Loop Policy Trees And EFE | Formalized | fep134_boolFeedback_strictlyBetter | Read invariantIn the explicit two-step Boolean model, observation-contingent feedback has value zero while every fixed open-loop second action has value one half. | Read assumptionsThis is a finite exact counterexample on fair Boolean observations and a mismatch terminal cost. It demonstrates possible feedback advantage, not a universal quantitative gap for active-inference agents. | Read non-vacuity reviewThe continuation action provably differs between false and true observations and the strict gap is exactly one half. | 2 / 0 / 1 |
|---|
fep-135Finite-Law Measure Embedding | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep135_embeddedLaw_apply_singleton | Read invariantA normalized finite law embeds as a weighted sum of Dirac measures that preserves every singleton mass and has native measure mass one. | Read assumptionsThe carrier is finite with its discrete measurable space. Finite real masses enter the native nonnegative-extended-real measure through ENNReal.ofReal; normalization and nonnegativity are inherited from FiniteLaw. | Read non-vacuity reviewAny nonuniform finite law gives distinct native singleton masses while the full measure remains normalized. | 2 / 0 / 1 |
|---|
fep-136Finite-Law Embedding Injectivity and Expectation Transfer | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep136_embeddedLaw_injective | Read invariantEquality of native weighted-Dirac measures reflects equality of the source finite laws, and native integration agrees exactly with the finite weighted expectation sum. | Read assumptionsThe carrier is finite and discretely measurable and observables are real-valued. Finiteness supplies integrability; no general integration or measure-equivalence theorem is inferred. | Read non-vacuity reviewDistinct point masses remain distinguishable by singleton evaluation and a nonconstant observable produces the same nontrivial expectation on both carriers. | 2 / 0 / 1 |
|---|
fep-137Embedded Finite-Kernel Composition | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep137_embeddedPredictive_eq_comp | Read invariantEmbedding finite prediction equals native composition of the embedded finite kernel with the embedded prior measure. | Read assumptionsInput and output carriers are finite and discretely measurable and each kernel row is normalized. The theorem is a carrier-transport identity, not a general disintegration or arbitrary-kernel approximation result. | Read non-vacuity reviewA nondegenerate prior and a state-dependent finite kernel yield a genuine mixture whose native singleton masses agree with finite prediction. | 1 / 0 / 1 |
|---|
fep-138Markov-Blanket Rectangle Factorization | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep138_staticJoint_rectangle_factorization | Read invariantEvery singleton rectangle of blanket, internal, and external coordinates in the embedded static joint has the exact blanket-marginal times two conditional-mass factorization. | Read assumptionsAll four carriers are finite and discretely measurable and the static model supplies normalized blanket and conditional laws. The theorem covers the discrete singleton generator and does not by itself state Mathlib conditional independence. | Read non-vacuity reviewThe correlated Boolean model contains two distinct positive blanket/joint atoms while retaining point-mass internal and external conditional rows. | 1 / 0 / 1 |
|---|
fep-139Native Markov-Blanket Conditional Independence | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep139_staticJoint_condIndepFun | Read invariantThe embedded finite blanket factorization satisfies Mathlib's native CondIndepFun predicate for internal and external coordinates conditioned on the sensory-active blanket coordinate. | Read assumptionsInternal and external carriers are nonempty; all carriers are finite, standard Borel through their discrete measurable structures, and the static model supplies exact normalized factorized rows. The proof identifies authored kernels with native conditional distributions and does not infer the result from zero finite mutual information. | Read non-vacuity reviewA Boolean model has two positive correlated blanket regimes and two distinct positive joint atoms; conditional independence is therefore not obtained by collapsing the whole measure to one point. | 2 / 0 / 1 |
|---|
fep-140Conditional Independence under Measurable Coarsening | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep140_condIndepFun_measurableImages | Read invariantNative blanket conditional independence is preserved under measurable images of both internal and external coordinates. | Read assumptionsThe source blanket theorem retains its finite, discrete, nonempty endpoint hypotheses and both image maps are explicitly measurable. The result is Mathlib's composition law and does not cover transformations of the conditioning coordinate. | Read non-vacuity reviewIdentity maps recover fep-139, while noninjective measurable coarsenings can merge endpoint states without invalidating conditional independence. | 1 / 0 / 1 |
|---|
fep-141Native Blanket-Transition Closure | Bayesian Mechanics | Finite To Native Blanket Transfer | Formalized | fep141_prediction_preserves_nativeBlanket | Read invariantEvery authored factorized transition row induces a next-state embedded law whose internal and external coordinates are natively conditionally independent given its next blanket. | Read assumptionsAll carriers are finite and discretely measurable and internal and external carriers are nonempty. The theorem is rowwise for one supplied current state; arbitrary mixtures over current-state uncertainty require additional hypotheses and are not claimed. | Read non-vacuity reviewA transition row may assign multiple positive next blanket regimes and nonconstant conditional endpoint laws while retaining the proved rowwise factorization. | 1 / 0 / 1 |
|---|
fep-142Finite Exponential-Family Normalization and Support | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep142_exponentialFamily_sum_one | Read invariantStrictly positive base weights normalize the finite scalar exponential family to a full-support probability law at every natural parameter. | Read assumptionsThe outcome carrier is finite and nonempty, base weights are strictly positive, and the sufficient statistic is real valued. No arbitrary manifold or multidimensional family is claimed. | Read non-vacuity reviewThe maintained nonconstant three-state family supplies unequal supported masses away from zero while retaining exact normalization. | 2 / 0 / 1 |
|---|
fep-143Affine Exponential-Family Log-Density Ratio | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep143_logDensityRatio_eq | Read invariantThe supported log-density ratio between two parameters is affine in the sufficient statistic with the exact log-partition difference. | Read assumptionsFiniteness, nonemptiness, and strict base-weight support make every logarithm ordinary and finite. The result is scalar and does not assert an extended-real identity at zero support. | Read non-vacuity reviewA nonconstant statistic and distinct parameters produce outcome-dependent log-density ratios. | 1 / 0 / 1 |
|---|
fep-144Finite Log-Partition Gradient | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep144_logPartition_hasDerivAt | Read invariantThe derivative of the finite scalar log-partition function equals the mean sufficient statistic. | Read assumptionsThe proof differentiates a finite sum of positive exponential weights and uses the positive partition denominator. It makes no infinite-sum exchange or general smooth-manifold claim. | Read non-vacuity reviewThe three-state statistic gives a nonconstant finite log-partition function whose mean changes with the parameter. | 1 / 0 / 1 |
|---|
fep-145Centered Exponential-Family Score Identity | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep145_score_eq_statistic_sub_mean | Read invariantThe scalar score is the sufficient statistic centered by its family mean and therefore has exactly zero expectation. | Read assumptionsThe score is defined on the finite full-support exponential family. This is a natural-parameter derivative identity, not a general score-regularity theorem for arbitrary likelihoods. | Read non-vacuity reviewA nonconstant statistic yields positive and negative centered scores across outcomes while their normalized weighted mean cancels exactly. | 2 / 0 / 1 |
|---|
fep-146Log-Partition Hessian–Variance–Fisher Identity | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep146_logPartition_secondDeriv_eq_variance | Read invariantDifferentiating the log-partition mean coordinate gives statistic variance, which equals scalar Fisher information; a concrete three-state family has variance two thirds at zero. | Read assumptionsThe result is the derivative of the already-proved first-derivative mean coordinate on a finite scalar family. Strict positivity is witnessed for a named nonconstant family and is not inferred for constant statistics. | Read non-vacuity reviewThe statistic (0,1,2) under unit base weights has variance two thirds, whereas every constant statistic has exactly zero variance and Fisher information. | 4 / 0 / 1 |
|---|
fep-147Exponential-Family KL–Bregman Identity | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep147_exponentialFamily_KL_eq_bregman | Read invariantFinite KL between two members of the same supported scalar exponential family equals the oriented Bregman divergence of the log-partition potential. | Read assumptionsThe carrier is finite and nonempty and strict base support supplies the logarithmic KL identity. The project finiteKL convention is totalized, but this theorem stays inside its ordinary full-support regime. | Read non-vacuity reviewThe companion three-state family has Fisher variance 2/3 at zero while the constant-statistic family has zero variance, so the underlying carrier has both curved and degenerate instances. Equal parameters give the zero-KL boundary by the shared finite-KL separation theorem; this row does not add a separate strict-KL witness for unequal parameters. | 2 / 0 / 1 |
|---|
fep-148Natural-to-Mean Coordinate Injectivity | Info Geometry | Finite Exponential Family Dual Geometry | Formalized | fep148_meanParameter_strictMono | Read invariantPositive statistic variance throughout a closed interval makes the natural-to-mean coordinate map strictly monotone and injective there. | Read assumptionsVariance positivity is an explicit interval premise. The theorem is local to a stated scalar interval and does not assert global dual-flat coordinates or positivity for degenerate statistics. | Read non-vacuity reviewThe three-state family supplies a strictly positive variance point, while the constant-statistic boundary shows why the positivity premise matters. | 2 / 0 / 1 |
|---|
fep-149Two-State Continuous-Time Markov Kernel | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep149_twoStateSemigroup_rowSum | Read invariantPositive two-state rates define a nonnegative transition matrix with every row summing to one for nonnegative time. | Read assumptionsThe state carrier is Boolean, both rates are strictly positive, and time is nonnegative. This is an exact two-state kernel rather than a general continuous-time Markov-chain construction. | Read non-vacuity reviewThe benchmark rates seven tenths and three tenths give decay rate one and a nonuniform stationary law. | 3 / 0 / 1 |
|---|
fep-150Continuous-Time Identity at Zero | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep150_twoStateSemigroup_zero | Read invariantThe exact two-state continuous-time transition matrix is the identity at time zero. | Read assumptionsBoth rates remain strictly positive through the maintained rate structure. The equality is entrywise on the Boolean carrier. | Read non-vacuity reviewDiagonal entries equal one and off-diagonal entries equal zero, so the result distinguishes all four transition entries. | 1 / 0 / 1 |
|---|
fep-151Two-State Chapman–Kolmogorov Semigroup | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep151_twoStateSemigroup_add | Read invariantThe exact two-state transition matrices satisfy the Chapman–Kolmogorov additive semigroup law entrywise. | Read assumptionsBoth times are nonnegative and rates are strictly positive. Composition is the finite Boolean matrix sum and no path-space or general generator existence theorem is inferred. | Read non-vacuity reviewPositive unequal rates and positive times produce nonidentity kernels whose matrix product still equals the transition at summed time. | 1 / 0 / 1 |
|---|
fep-152Two-State Continuous-Time Master Equation | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep152_twoStateSemigroup_hasDerivAt | Read invariantEvery transition entry is differentiable and its derivative equals both the generator-times-transition and transition-times-generator finite sums. | Read assumptionsThe generator and transition matrices are the maintained explicit Boolean formulas. This proves the forward and backward master equations for one two-state semigroup, not a general CTMC existence theorem. | Read non-vacuity reviewPositive unequal rates give nonzero off-diagonal derivatives away from stationarity and exercise both left and right generator products. | 1 / 0 / 1 |
|---|
fep-153Continuous-Time Stationarity and Detailed Balance | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep153_twoStateSemigroup_stationary | Read invariantThe explicit stationary law is invariant under every nonnegative-time transition and satisfies detailed balance entrywise. | Read assumptionsBoth rates are strictly positive and time is nonnegative. Reversibility is proved only for this exact two-state family and does not cover driven or nonequilibrium generators. | Read non-vacuity reviewUnequal benchmark rates produce a nonuniform stationary law while still balancing the two opposing fluxes. | 2 / 0 / 1 |
|---|
fep-154Exact Two-State Exponential Relaxation | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep154_twoStateRelaxation_exact | Read invariantThe true-state mass of any initial Boolean law relaxes toward stationarity by the exact factor exp(-(a+b)t). | Read assumptionsRates are positive, time is nonnegative, and prediction uses the explicit two-state transition. This is exact finite-state relaxation, not a mixing theorem for arbitrary chains. | Read non-vacuity reviewThe benchmark point mass differs from the nonuniform stationary law, so the decaying deviation starts nonzero. | 2 / 0 / 1 |
|---|
fep-155Exact Two-State Quadratic Lyapunov Decay | Thermodynamics | Two State Continuous Time Thermodynamics | Formalized | fep155_twoStateLyapunov_exact | Read invariantSquared deviation from stationarity decays by exp(-2(a+b)t), and its exact derivative is minus twice the decay rate times the Lyapunov value. | Read assumptionsThe Lyapunov function is the scalar square of the true-state mass deviation for the explicit two-state semigroup. It is not a general entropy-production or physical free-energy theorem. | Read non-vacuity reviewThe benchmark nonstationary point mass has a strictly negative Lyapunov derivative at time zero. | 3 / 0 / 1 |
|---|
fep-156Planning as Inference: the EFE Policy-Selection Bridge | Active Inference | Standalone EFE Formalizations | Formalized | fep156_boltzmann_control_posterior_minimizes_efe | Read invariantOn a finite policy carrier with fixed precision, the KL-regularized control objective (expected EFE plus inverse-precision KL to the prior) is minimized exactly by the Boltzmann control posterior proportional to prior * exp(-gamma * G); the minimized value is -gamma^-1 log Z, the EFE splits as risk plus ambiguity, and the finite and treewise argmin views agree. | Read assumptionsThe bridge is a finite-carrier Gibbs/Donsker-Varadhan statement about the EFE control objective; it is not a general planning algorithm or a continuous-action result, and the policy-tree agreement is restricted to the treewise value surface of the policy_tree module. | Read non-vacuity reviewThe finite argmin exists and attains the closed-form Boltzmann value -gamma^-1 log Z for nonempty policy sets. | 9 / 0 / 1 |
|---|
fep-157The Perception-Action Loop as a Closed-Loop Active-Inference Theorem | Active Inference | Standalone EFE Formalizations | Formalized | fep157_loop_invariant_surprisal_bound | Read invariantEach closed-loop perception-action step is non-increasing in belief surprisal: the step's KL splits exactly into predictive and posterior parts, prediction contracts the predictive distribution (Dobrushin), and the loop invariant bounds surprisal by its initial value plus accumulated expected free energy; the loop's fixed point is the Boltzmann control posterior and equals the policy posterior of the control-as-inference view. | Read assumptionsThe loop is a finite-state kernel composition; positivity statements assume full-support likelihoods and supporting posteriors, and the contraction is the finite Dobrushin-coefficient statement, not a continuous-state or neural-implementation claim. | Read non-vacuity reviewThe strict step-wise KL decrease holds on the full-likelihood witness kernels, and at the fixed point the loop posterior coincides with the Boltzmann control posterior. | 13 / 0 / 1 |
|---|
fep-158Bayesian Model Reduction | Active Inference | Standalone EFE Formalizations | Formalized | fep158_reduction_free_energy_monotone | Read invariantMasking evidence never lowers the model evidence: the reduced model's evidence free energy dominates the full model's, the reduced posterior obeys the multiplicative Bayes-odds law with the evidence weight and reconstructs the full posterior through the evidence ratio, and the Gibbs-certificate excess over the optimizer is exactly the KL divergence to it. | Read assumptionsThe reduction statements hold for finite measure spaces with the pinned Donsker-Varadhan duality; the Gaussian log Bayes factor is stated in the pinned natural chart of the information-geometry module and is not a generic asymptotic model-selection claim. | Read non-vacuity reviewThe masked predictive is bounded by the full evidence, and the reduced posterior reconstructs the full posterior exactly through the evidence ratio. | 10 / 0 / 1 |
|---|
fep-159EFE and Entropy-Production Time-Scale Separation | Active Inference | Standalone EFE Formalizations | Formalized | fep159_epistemic_gain_bounded_by_affinity | Read invariantThe two-state belief information gap is bounded by the entropy-production rate scaled by the relaxation time (gain at most production/decay), the evolved gap contracts to the invariant measure no slower than the relaxation timescale, the one-slice path-space entropy production equals (1 - rho) * sigma / decay, and under the 1/eps rate scaling the evolved gain after any fixed positive action time vanishes. | Read assumptionsAll statements are for the explicit two-state continuous-time semigroup and its scaled one-parameter family; the slice-path identity is the one-slice restriction of the path-thermodynamics production, not a general path-space theorem. The ness_flow import is an orphan-adoption marker with no mathematical dependence. | Read non-vacuity reviewThe bound is attained by the stationary law for the benchmark rates, and the fast-relaxation limit exhibits the vanishing exactly. | 9 / 0 / 1 |
|---|
fep-160Helmholtz–Ao Decomposition of Nonequilibrium Steady Currents | Active Inference | Standalone EFE Formalizations | Formalized | fep160_aoDecomposition | Read invariantOn a finite state space with a full-support stationary law, every rate field decomposes exactly into a reversible part (detailed-balanced relative to the law) plus a circulation part (skew in the law-weighted sense); the stationary edge current equals twice the law-weighted circulation part, the reversible part carries no current, removing the circulation part is exactly detailed balance, the log-affinity splits into the Ao-potential drop plus the skew force, stationarity makes the node divergence of the stationary current vanish, and the directed three-cycle witness is stationary, divergence-free, and circulating. | Read assumptionsAll statements are finite-carrier algebra: the Ao potential is the pointwise -log p* mass field and is deliberately distinct from the thermodynamic Helmholtz free energy of fep-013; the continuum Fokker-Planck equation, a state-dependent diffusion matrix field, and SDE noise are not formalized. Stationarity and the probability current reuse the established FEP.ContinuousTimeMarkov generator contract. | Read non-vacuity reviewThe decomposition is unconditional for every rate field under the full-support hypothesis, and the directed three-cycle exhibits a genuine NESS whose circulation part is 1/2 at the forward edge. | 13 / 3 / 1 |
|---|
fep-161Skew Bilinear Cancellation of the Trace and Quadratic Terms | Thermodynamics | Geometric Mechanics Notation | Formalized | fep161_skewTrace_eq_zero | Read invariantA skew-symmetric matrix contracted against a symmetric matrix has zero trace, and a skew-symmetric matrix annihilates its own quadratic form: the two algebraic cancellations behind the manuscript's solenoidal expansion, holding unconditionally on the stated symmetry hypotheses. | Read assumptionsPlain finite real matrices indexed by Fin n with explicit pointwise symmetry hypotheses; no continuum Hessian, no smoothness structure, and no numerical witness is claimed. | Read non-vacuity reviewBoth cancellations are exact identities on their hypothesis classes, witnessed by any nonzero skew matrix against a nonzero symmetric one. | 2 / 0 / 1 |
|---|
fep-162The Discrete Hessian as a Symmetrization Construction | Thermodynamics | Geometric Mechanics Notation | Formalized | fep162_skewTrace_symmetrize_eq_zero | Read invariantSymmetrization of raw mixed-difference data constructs a symmetric discrete Hessian (the finite Clairaut property as a construction), the trace cancellation holds against the constructed matrix with no hypothesis on the raw data, and on already-symmetric data the construction is the identity. | Read assumptionsThe construction replaces the continuum Clairaut theorem by finite algebra; it does not claim differentiability, a continuum Hessian, or convergence of mixed-difference quotients. | Read non-vacuity reviewThe symmetrized matrix is symmetric for every input and coincides with the given matrix exactly on the symmetric subclass. | 3 / 0 / 1 |
|---|
fep-163The Three-Term Solenoidal Expansion and Its Conditional Drop | Thermodynamics | Geometric Mechanics Notation | Formalized | fep163_solenoidal_expansion | Read invariantThe weighted divergence of the candidate current decomposes exactly into the trace slot, the transport-divergence slot, and the density coupling slot; under the stationary coupling the identity reads tr(Q H) - g^T Q g + (div Q)^T g; both cancellable terms die on the skew and symmetric hypotheses, and the remaining drop holds only under an explicit extra hypothesis (orthogonality or spatially constant Q), with a concrete remainder datum where it does not. | Read assumptionsDirectional derivative data is explicit (H for the Hessian slot, DQ for the transport-divergence slot); the coupling is an explicit hypothesis, not a solved PDE; the weighted divergence is defined by the exact Leibniz decomposition rather than a discretization of Fokker-Planck. | Read non-vacuity reviewThe remainder witness evaluates to exactly 1 on concrete two-direction derivative data, so the unconditional drop is not vacuously unreachable. | 5 / 1 / 1 |
|---|
fep-164Graph Divergence of the Candidate Solenoidal Current | Thermodynamics | Geometric Mechanics Notation | Formalized | fep164_graphDecomposition | Read invariantOn a finite node set the node divergence of the skew transport field is twice its row sum; the node divergence of the edge current splits into the transport slot plus the discrete-divergence slot; and the weighted node divergence obeys an exact Leibniz rule whose p-residual does not vanish by skewness alone. | Read assumptionsEdge fields are plain real matrices with the flux convention W i j = flux i to j; the weighted statements assume a strictly positive density; no continuum graph limit or first-order asymptotic identification is claimed. | Read non-vacuity reviewThe decomposition and the Leibniz rule are exact on every finite node set, and the residual term is generically nonzero by nodeDiv_skew. | 4 / 0 / 1 |
|---|
fep-165Necessity Witness for the Unconditional Solenoidal Drop | Thermodynamics | Geometric Mechanics Notation | Formalized | fep165_witness_drop_fails | Read invariantFor the exact 2-node transport matrix [[0,1],[-1,0]] and gradient (1,0) the candidate current is (0,-1), the discrete divergence of the transport field is (2,-2), the node divergence of the current is (1,-1), and in particular equals 1 at node 0: the unconditional solenoidal drop is false, and neither the orthogonality nor the constant-Q hypothesis is available on this witness. | Read assumptionsA concrete finite counterexample only; it shows the manuscript's honesty guard is necessary rather than decorative and claims nothing about systems satisfying the extra hypotheses of fep-163. | Read non-vacuity reviewThe witness evaluates to exactly 1 at node 0, refuting the unconditional drop on its exact hypothesis class. | 5 / 0 / 1 |
|---|
fep-166Uniqueness of the Law-Weighted Reversible/Circulation Split | Active Inference | Standalone EFE Formalizations | Formalized | fep166_split_unique | Read invariantAny competing pair S, A with W = S + A, p-weighted reversibility of S and p-weighted skewness of A coincides pointwise with the canonical symmetricPart and circulationPart of the rate field; the reversible boundary is in uniqueness form (a p-reversible field has the split (W, 0)), and on the concrete two-state datum the constraint-satisfying split is the canonical one with genuinely nonzero forward circulation 1/2 and strictly negative reverse entry -1/4. | Read assumptionsPositivity of the finite law is the only analytic input and licenses the divisions; no stationarity hypothesis, no generator contract, and no nonnegativity claim for the circulation part enter the statements. | Read non-vacuity reviewThe t-0060 datum with weight law p = (1/3, 2/3) and rate entries 1, 5/2, 3/4, and -1 satisfies every constraint clause, its split is forced to be the canonical one, and the circulation entries 1/2 and -1/4 are computed exactly, so the uniqueness characterization is exercised on nontrivial data. | 7 / 0 / 1 |
|---|
fep-167Frobenius Least-Squares Projection of the Symmetrizer | Thermodynamics | Geometric Mechanics Notation | Formalized | fep167_frobenius_pythagoras | Read invariantFor symmetric S the squared Frobenius norm splits exactly as ||H - S||^2 = ||H - symmetrize H||^2 + ||symmetrize H - S||^2, the symmetrizer minimizes the squared distance among symmetric matrices with equality exactly at the symmetrizer, the symmetric minimizer is unique, and the concrete nonsymmetric datum [[0,1],[0,0]] carries residual exactly 1/2. | Read assumptionsMatrix projection only, no differentiability, no continuum Clairaut theorem, no Bregman-projection existence/uniqueness claim. | Read non-vacuity reviewThe residual example evaluates to exactly 1/2 on nonsymmetric data, and symmetric data attains the zero residual exactly at the symmetrizer, so both the strict and the degenerate boundary are realized. | 4 / 0 / 1 |
|---|
fep-168Quantitative Control of the Uncancelled Divergence Remainder | Thermodynamics | Geometric Mechanics Notation | Formalized | fep168_weightedDivergence_eq_remainderDot | Read invariantOn the fep-163 carrier the weighted divergence equals dot (divQ DQ) g under the cancellation hypotheses, the squared Cauchy-Schwarz budget (weightedDivergence)^2 <= (sum r_i^2)(sum g_i^2) bounds the uncancelled remainder with its abs-product corollary, and equality is attained on aligned nonzero data with norm(g)^2 = 1. | Read assumptionsQuantitative budget on the fep-163 finite derivative-data carrier; the coupling hypothesis is sufficient-not-necessary (slot = dot(Qg, dlogp)); no PDE-discretization or entropy-production claim. | Read non-vacuity reviewThe aligned datum Q = [[0,1],[-1,0]], H = diag(1, 2), DQ with divQ (1, 0), and g = (1, 0) attains the budget with equality, while the pinned remainderG = (1, 1) datum is strict with gap 1, so both the equality and the strict boundary are realized. | 4 / 0 / 1 |
|---|