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.
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
- State-Dependent Observation Noise Reintroduces Epistemic Value in Linear-Gaussian Active Inference, Daniel Corva, 2026-07-22
Pre-registered gates
| Gate | Claim | Outcome | Tier and warrant |
|---|---|---|---|
| C1 · calibration zero | With p = p* and an exact filter, misspecification and the inference gap both sit below 1e-12.Registered e01f89e | exact | |
| C2 · misspecification isolation | Misspecify the model and keep inference exact. D_KL[p* ‖ p] is positive and stable, and the gap stays below 1e-12.Registered e01f89e | exact / bounded | |
| C3 · inference-gap isolation | Keep p = p* and degrade inference. The gap is positive, and misspecification stays below 1e-12.Registered e01f89e | exact / bounded | |
| C4 · additivity | The floor, misspecification and the gap rebuild the measured E[F] within the four-term bound.Registered e01f89e | exact | |
| C5 · incompleteness demonstration | Two agents the collapsed accounting scores identically at a matched E[F], which the instrument separates.Registered e01f89e | exact / 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 | bounded | |
| D1 · fidelity-ladder ordering | Along five rungs, from plug-in R(μ⁻) to the exact reference, the inference gap decreases at a certified tolerance.Registered b646cb6 | bounded | |
| D1 · first reading, four orderings | The same ordering read against measured bars, before a certified tolerance exists.Registered ac9fbc5, measured bf34ea0 | computedCORROBORATED | |
| D1 · route 6, derivative-of-covariance terms | The derivative-of-covariance terms are visible as a resolved difference.Registered ac9fbc5, measured bf34ea0 | computedCORROBORATED | |
| D1 · route 6, iteration | The iteration is visible as a resolved difference.Registered ac9fbc5, measured bf34ea0 | computedCORROBORATED | |
| D2 · scaling exponent | The fitted σ-exponent lies in 2 ± 0.5, inside a fit window shown to be non-empty first.Registered fc8aac4 | bounded | |
| D3 · fourth falsifier, extension to {−4,…,2} | Extending the action set gives H* ≤ 6. Measured H* = 6.Registered 86d1f22, measured 17a1be7 | boundedPROVED | |
| D3 · fourth falsifier, refinement at step 0.5 | Refining the action set moves H* by at most 1. Measured |ΔH*| = 0.Registered 86d1f22, measured 3619016 | boundedPROVED | |
| D3 · fourth falsifier, refinement at step 0.25 | Refining the action set moves H* by at most 1. Measured |ΔH*| = 0.Registered 86d1f22, measured c37fac3 | boundedPROVED | |
| D4 · c₄ out of sample, exp(x) and sin | The G4b exponent sits within 0.25 of 6.Registered 38e2963, measured d267382 | boundedCORROBORATED | |
| D4 · c₄ out of sample, tanh | The G4b exponent sits within 0.25 of 6. Measured σ^6.302 against a 0.25 bar.Registered 38e2963, measured d267382 | boundedCORROBORATED | |
| D4 · certified discretisation bound (GATE-D4) | The R6 gap exceeds the registered threshold T = 5.962e−4 nats.Registered 8de86a3 | bounded | |
| E1 · vs dual control, fixed-R signature | Certainty equivalence holds exactly with fixed R, J_CE = J*.Registered e01f89e | exact | |
| E1 · vs dual control, R(x) leg | With state-dependent R beyond horizon 1, the agent beats certainty equivalence, J_agent < J_CE.Registered e01f89e | bounded |
Verified at release
| Cell | Claim | Tier | Release |
|---|---|---|---|
| A1 · flat epistemic term | With fixed R, per-step epistemic value is constant across policies to machine precision. | exact | v0.4.2 |
| A2 · flattening reproduction | With fixed R, a fixed-gain Kalman schedule reproduces the posterior for every policy. | exact | v0.4.2 |
| A3 · structural, not accidental | The collapse survives any perturbation of A, B, C, Q and of the value of a fixed R. | exact | v0.4.2 |
| B1 · dual effect (H3) | State-dependent R makes the posterior covariance depend on the policy. | bounded | v0.4.2 |
| B2 · determinant-visibility (H3′) | Epistemic value varies across policies. Checked for scalar observations. | bounded | v0.4.2 |
| B3 · the Remark 4 knife-edge | On an exact level set the covariance moves while epistemic value stays ½ ln 3.Check added at a40a156 | bounded | v0.4.3 |
| B4 · behavioural dissociation | Only the state-dependent agent reads the cue, learns the context and crosses. Its check asserts every such action, since v0.4.3. | bounded | v0.4.3 |
| B5 · no-flattening witness | Flattening is refused under state-dependent R with a mean-shifting coupling, before any data. | bounded | v0.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.