p*: certifiable active inference

The free energy principle's standard derivation lets one distribution play both the agent's model and the world, so a wrong model has nowhere to show up. Hold the two apart. How much free energy does an agent then pay for being wrong about the world, and how much for being wrong about what its own model implies? How tightly can each be certified?

The accounting under test splits expected free energy into a floor, a misspecification term and an inference gap. The standard accounting identifies the model with the true process and collapses all three to the floor. Every cell drives its agents with a common exogenous action sequence, so no result here reads as closed-loop. No test claims more than its prover licenses.

𝔼p∗(⋅|u)[F]=H(p∗(⋅|u))⏟floor+DKL[p∗(y|u)‖p(y|u)]⏟misspecification+𝔼p∗(⋅|u)[DKL[q(x)‖p(x|y)]]⏟inference gap\mathbb{E}_{p^*(\cdot\mid u)}[F] = \underbrace{H\big(p^*(\cdot\mid u)\big)}_{\text{floor}} + \underbrace{D_{\mathrm{KL}}\big[p^*(y\mid u)\,\|\,p(y\mid u)\big]}_{\text{misspecification}} + \underbrace{\mathbb{E}_{p^*(\cdot\mid u)}\Big[D_{\mathrm{KL}}\big[q(x)\,\|\,p(x\mid y)\big]\Big]}_{\text{inference gap}}

The programme keeps its claims certifiable with warrantlib. Its measured rows come from checks that report in warrantlib's vocabulary, which fills the tier and warrant columns. warrantlib refuses a PROVED report that does not name the commit that registered its bar and the commit that measured it.

Papers

Pre-registered gates

As of . Commits are in inferogenesis/cpomdp.
GateClaimOutcomeTier and warrant
C1 · calibration zeroWith p = p* and an exact filter, misspecification and the inference gap both sit below 1e-12.Registered e01f89e Pendingexact
C2 · misspecification isolationMisspecify the model and keep inference exact. D_KL[p* ‖ p] is positive and stable, and the gap stays below 1e-12.Registered e01f89e Pendingexact / bounded
C3 · inference-gap isolationKeep p = p* and degrade inference. The gap is positive, and misspecification stays below 1e-12.Registered e01f89e Pendingexact / bounded
C4 · additivityThe floor, misspecification and the gap rebuild the measured E[F] within the four-term bound.Registered e01f89e Pendingexact
C5 · incompleteness demonstrationTwo agents the collapsed accounting scores identically at a matched E[F], which the instrument separates.Registered e01f89e Pendingexact / bounded
C6 · breaking the calibration zero under R(x)Correct model, plug-in inference, state-dependent R. The gap is positive and separated from the certified error.Registered e01f89e Pendingbounded
D1 · fidelity-ladder orderingAlong five rungs, from plug-in R(μ⁻) to the exact reference, the inference gap decreases at a certified tolerance.Registered b646cb6 Pendingbounded
D1 · first reading, four orderingsThe same ordering read against measured bars, before a certified tolerance exists.Registered ac9fbc5, measured bf34ea0 FAIL(3 of 4 fired)computedCORROBORATED
D1 · route 6, derivative-of-covariance termsThe derivative-of-covariance terms are visible as a resolved difference.Registered ac9fbc5, measured bf34ea0 PASScomputedCORROBORATED
D1 · route 6, iterationThe iteration is visible as a resolved difference.Registered ac9fbc5, measured bf34ea0 PASScomputedCORROBORATED
D2 · scaling exponentThe fitted σ-exponent lies in 2 ± 0.5, inside a fit window shown to be non-empty first.Registered fc8aac4 Pendingbounded
D3 · fourth falsifier, extension to {−4,…,2}Extending the action set gives H* ≤ 6. Measured H* = 6.Registered 86d1f22, measured 17a1be7 PASSboundedPROVED
D3 · fourth falsifier, refinement at step 0.5Refining the action set moves H* by at most 1. Measured |ΔH*| = 0.Registered 86d1f22, measured 3619016 PASSboundedPROVED
D3 · fourth falsifier, refinement at step 0.25Refining the action set moves H* by at most 1. Measured |ΔH*| = 0.Registered 86d1f22, measured c37fac3 PASSboundedPROVED
D4 · c₄ out of sample, exp(x) and sinThe G4b exponent sits within 0.25 of 6.Registered 38e2963, measured d267382 PASSboundedCORROBORATED
D4 · c₄ out of sample, tanhThe G4b exponent sits within 0.25 of 6. Measured σ^6.302 against a 0.25 bar.Registered 38e2963, measured d267382 FAIL(fired)boundedCORROBORATED
D4 · certified discretisation bound (GATE-D4)The R6 gap exceeds the registered threshold T = 5.962e−4 nats.Registered 8de86a3 Pendingbounded
E1 · vs dual control, fixed-R signatureCertainty equivalence holds exactly with fixed R, J_CE = J*.Registered e01f89e Pendingexact
E1 · vs dual control, R(x) legWith state-dependent R beyond horizon 1, the agent beats certainty equivalence, J_agent < J_CE.Registered e01f89e Pendingbounded

Verified at release

Verified at release, not pre-registered. Each cell names the release its check shipped in.
CellClaimTierRelease
A1 · flat epistemic termWith fixed R, per-step epistemic value is constant across policies to machine precision.exactv0.4.2
A2 · flattening reproductionWith fixed R, a fixed-gain Kalman schedule reproduces the posterior for every policy.exactv0.4.2
A3 · structural, not accidentalThe collapse survives any perturbation of A, B, C, Q and of the value of a fixed R.exactv0.4.2
B1 · dual effect (H3)State-dependent R makes the posterior covariance depend on the policy.boundedv0.4.2
B2 · determinant-visibility (H3′)Epistemic value varies across policies. Checked for scalar observations.boundedv0.4.2
B3 · the Remark 4 knife-edgeOn an exact level set the covariance moves while epistemic value stays ½ ln 3.Check added at a40a156boundedv0.4.3
B4 · behavioural dissociationOnly the state-dependent agent reads the cue, learns the context and crosses. Its check asserts every such action, since v0.4.3.boundedv0.4.3
B5 · no-flattening witnessFlattening is refused under state-dependent R with a mean-shifting coupling, before any data.boundedv0.4.2

How D3 was measured

38df72d registered a statistic between two fixed constant policies, a reach and a walk, with its sign convention, its horizon-1 anchors and four falsifiers. That registered pair found no crossover.

The exhaustive search landed later the same day, at b077372. Its result is measured, not pre-registered. The open-loop exhaustive argmin flips from reach to walk at H* = 7 on the action set {0, ±1, ±2}. That 7 is an upper bound. On any action set containing −3, H* = 6.

D3’s fourth falsifier was registered at 86d1f22 before any of its cells ran. It passed on both axes, as the table shows.