Verification-layer probe · scale-free certificate, nano proof · sound-verified

One Energy, Both Roles

Can a single scalar energy be the controller and its own stability certificate — with no tax? A falsifiable probe, from a saturated line to a 4D cart-pole.

Charlot Lab, Institute for Physical AI @ BMI

Draft · 2026-07 · every figure below is a sound proof, an audited result, or a negative result · companion to Energy Is the Certificate

Sound-verified · 2D → 4D · self-controlled Learned ≻ quadratic · SMT-proven (dReal) Internal · certificate dimension-free · proof nano · sim

The Energy First Architecture wagers that one learned scalar energy $E(s)$ is not a loss term but the whole controller: the action descends it, and the same function is a Lyapunov certificate that provably contracts along the closed loop. We test the sharp, falsifiable form — is there a tax between the two roles? — on a ladder of plants, verifying every certificate soundly (worst-case over the continuum, not sampled). The result: one energy carries both roles with no measurable tax, from a saturated double integrator, through a nonlinear torque-underactuated pendulum (audited, seed-robust, and re-proved on a pure-Rust fabric in ~5 ms), up to a 4D underactuated cart-pole. And where a learned energy is genuinely warranted — a non-convex region of attraction — a counterexample-hardened learned energy certifies a strictly larger sound region than any quadratic ($R=1.80$ vs $1.60$), proven exactly by an SMT solver. Three tempting negatives were each overturned by a more decisive test; the through-line is that sampled agreement is not soundness.

1 · The claim, and the tax

A world model that predicts, scores, and commits gives an expected-value ranking, not a guarantee. EFA's answer is to make the object an agent descends to act the very same object that certifies the action: the controller is greedy, $u^*(s)=\arg\min_u E\!\left(f(s,u)\right)$, and the certificate is that $E$ contracts, $E(f(s,u^*))-E(s)<0$, over a region. The falsifiable question is whether one energy can be good at both at once, or whether forcing it to certify costs controller quality (or vice-versa) — a unification tax. We measure it, and we make the certificate a proof rather than a sample.

2 · The ladder, sound-verified

Each row is one energy playing both roles on one plant. “Sound certificate” means proven over the continuum — adaptive second-order Taylor + interval-Hessian (CROWN) box refinement, or an SMT solver — not a sampled score.

System	Dim	Control	Sound certificate	Note
Saturated double integrator	2D	100%	proven	where a plain quadratic fails; tax = 0 both directions
Pendulum, adequate torque	2D	100%	proven · audited	zero tax; seed-robust; on the Ferric fabric (~4.9 ms re-proof)
Weak-torque pendulum (swing-up+capture)	2D	100%	proven · audited	“tax” was a value-iteration artifact — a direct CLF unifies it
Cart-pole, quadratic energy	4D	100%	proven · audited	signed Hessian cancellation was the key
Cart-pole, learned energy	4D	100%	proven · audited	head small — a quadratic already suffices on a smooth plant
Reversed-VdP · learned ≻ quadratic	2D	100%	SMT-proven	1.80 > 1.60 once CEGIS-hardened; plain learned = worse (holes)
N-link arm · port-Hamiltonian (structure, not proof)	≤ 24	100%	by construction	V̇≤0 to machine precision at a 24-dim state; box/SMT proof dies at ~8D; survives a learned residual
7-DOF arm · necessity gate on a real OOD policy	14	—	discrete barrier	a real BC policy is unsafe OOD (2951/12000); the gate vetoes → 0/12000, 159 µs, minimum-intervention
MuJoCo arm · gate on a real robot body	8	—	real dynamics	energy from MuJoCo's own $M(q)$; structural identity 1.5e-9; naive policy 4263/6000 → gate 0/6000, zero unrecoverable, at the real dt
MuJoCo arm striking a floor · contact	8	—	holds / located	dissipative impact: gate 0/6000 through 522 contact-steps, robust to a 3× wrong contact model; elastic impact leaks (406 vs 412, right-or-wrong model — not model error; contact is passive) — natural passive energy (~7×, 309→42) + approach-anticipating barrier + control authority reach 10/6000 (~30×); the residual is mostly a controllability limit (torque sweep 39→10), not a certificate gap
Acrobot · underactuated (1 actuator / 2 DOF)	4	—	actuator passivity	the actuator is the only energy port, so damping it gives $\dot E\le0$; agent holds $\{E\le c\}$ 100% vs an energy-pump 17.8%, at 16× lower J/VT — the natural-energy certificate needs no arbitrary Lyapunov shaping
Hopper · underactuation + contact	2+	—	combined	passive hop-height + one leg + foot make/break; certificate holds both dissipative and energy-storing ground, agent 100% vs pump 53%, ~5× lower J/VT; no new frontier
Planar humanoid · floating base + multi-contact	7	—	scales	3-DOF unactuated base + 4 leg actuators; same natural energy via multiple ports — agent 100% / 824 W vs an energy-pump 19.8% / 13427 W

One scalar, read two ways

start position =

step size =

worst $\dot V$ along the run:

The gold curve is one scalar energy. Descending it is the controller — that is the ball moving. Reading its change along the same motion is the certificate: while each step goes downhill, $\dot V \le 0$ and the loop provably cannot diverge. There is no second object here and no separate verifier; the proof is the objective. Now push the step size up: too large a step overshoots, $\dot V$ turns positive, and the certificate reports it — which is the gate refusing rather than the controller failing quietly.

3 · What “both roles, soundly” means

For any single action the closed loop is a known map, so the greedy controller is an OR over actions: a box is soundly certified if some action makes $E(f(s,u))-E(s)+\alpha\lVert s\rVert^2<0$ over the whole box, and greedy is at least that good. Each action's term is bounded by a second-order Taylor model at the box center plus an interval Hessian (CROWN for the tanh head), refined adaptively. The nonlinear plants required the state-dependent Jacobian and dynamics-Hessian terms; the 4D plant required keeping the signed $J^\top\!PJ-P$ cancellation rather than inflating to absolute values. Where a learned energy's tanh head defeats the interval bound, a δ-complete SMT solver (dReal) verifies the same query exactly.

4 · Three negatives, each overturned

The result is trustworthy only because the walk-backs went toward the truth. Each of these was recorded as a negative, kept under scrutiny, and reversed by a more decisive test.

The weak-torque “tax.” Claimed: control needs lookahead a one-step certificate cannot express. Reversed: it was the value-iteration objective — a direct control-Lyapunov energy unifies it, seed-robust.
The 4D wall. Claimed: the curse of dimensionality stops the sound proof. Reversed: a loose bound; keeping the signed Hessian cancellation converged it (failing boxes $47\%\!\to\!0$).
Learned ≺ quadratic. Observed: a learned energy sampled-contracts more (98% vs 91%) yet certifies 0 — real holes the solver finds. Reversed: harden the holes shut → learned ≻ quadratic.

The through-line, stated once: sampled contraction ≠ sound contraction. The energy that looks best by sampling can be the worst certificate; only a worst-case proof distinguishes them.

5 · Where a curve is warranted, close its holes

On a plant whose region of attraction is non-convex — an actuated reversed Van der Pol, where a quadratic ellipse provably cannot match the basin — a learned energy should win, but only if it is sound everywhere, not on average. The counterexample-guided loop makes it so: train the energy, ask the solver for a state where the greedy controller fails, fold that counterexample back into training, retrain, repeat — self-controlled throughout.

Quadratic: smooth, no bumps — certifies to radius 1.60, self-controlled.
Learned, plain: better average contraction, but local tanh bumps → real holes the solver finds → certifies 0.0.
Learned, CEGIS-hardened: holes sewn shut (outer edge, then near-origin bumps) → certifies 1.80 — a strictly larger sound region than any quadratic, dReal-proven ($\delta=10^{-4}$).

This is the first demonstration of learned ≻ quadratic in the self-controlled unification setting, not merely fixed-control certification — the positive direction of the certificate program's §5 law, carried into the one-energy regime.

6 · Structure, not proof — off the toys

Everything above earns the certificate by proving it, which walls out at ~4–8 dimensions. The physics-first move is to earn it by construction: structure the energy as a port-Hamiltonian, and on a planar $N$-link arm under energy-shaping control the closed-loop energy satisfies — exactly, by the manipulator identity $\dot q^\top(\tfrac12\dot M - C)\dot q = 0$ — $\dot V = -\dot q^\top K_d\, \dot q \le 0$, analytic, O(1), at any $N$. Verified to machine precision at a 24-dimensional state (control 100% throughout), invariant to an arbitrary learned potential residual (learn the residual, keep the guarantee), where a box/SMT proof would need $\sim\!10^{31}$ boxes. Structure gives at any dimension what proof cannot give past ~8D.

That is what makes the point — necessity. A robot's wrong action has physical consequences; the incumbent commit rule is an expected-value score, never a guarantee before commit. On a 7-DOF arm, a real behavior-cloned policy is safe in-distribution and — like every data-first policy — unsafe out-of-distribution (leaving the safe envelope $2951/12000$ steps). A discrete control-barrier gate built on the energy admits an action only if its actual discrete next-state stays in $S=\{V\le c\}$, else vetoes it for an energy-shaping fallback proven to supply an admissible action — so $S$ is forward-invariant at the real time-step, by construction. Result: violations 2951 → 0, at 159 µs per step, and minimum-intervention (zero vetoes in-distribution — it overrides only where the policy is actually unsafe). The certificate supplies the guarantee the policy's score cannot, exactly where the policy fails.

The same gate then moves onto a real robot body — a MuJoCo arm with real inertia, motor armature and torque-limited motors, the energy built from MuJoCo's own mass matrix $M(q)=\texttt{mj\_fullM}$ and bias forces. The structural identity holds to 1.5×10⁻⁹ on the real dynamics; a naive policy leaves the envelope 4263/6000 steps, the certificate holds it 0/6000 with zero unrecoverable vetoes, at the real time-step. Two subtleties surface on the real body and are handled, not hidden: correct energy-shaping compensates gravity only and keeps Coriolis (so skew-symmetry cancels it — canceling the full bias leaves a residual), and under torque limits the safe set needs a barrier buffer to retain braking authority near its edge.

Scope, drawn correctly. In simulation, and "small" is not the limit — the certificate is lightweight by design and wraps a full-scale policy it did not train. The structural (port-Hamiltonian) certificate is dimension-free for fully-actuated bodies — an exact identity, verified past a 24-dim state, and the algebra does not stop there. What is genuinely bounded is narrower: the exhaustive sound-proof of a learned energy is nano (state dimensions 2–4, few-seed, specific plants — saturated double integrator, pendulum, cart-pole, reversed Van der Pol; worst-case over the continuum via adaptive Taylor+CROWN or exact SMT), which is exactly why we move to structure, not proof; underactuated bodies re-introduce the hard part. The necessity gate now runs on a real MuJoCo body against a policy stand-in — the one increment left in the decider is a real released external VLA in the same loop (its weights are on disk; the gate is embodiment-agnostic, so that is runtime integration, not a change to any proof here). Contact-rich manipulation certification remains the open frontier — and we can now say why, from measurement. On a MuJoCo arm striking a floor, the one-step energy barrier holds through dissipative impacts (and is robust to a wrong contact model, because an impact removes energy). An energy-storing (elastic) contact leaks it — but the cause is not what one first guesses: the leak is the same whether the contact model is right or wrong (406 vs 412), a longer horizon barely helps, and the contact is itself passive (total mechanical energy never exceeds its release value). The real cause is the certificate choice: $V=\tfrac12\dot q^\top M\dot q + V_{\text{task}}$ is not the quantity the contact is passive with respect to — energy-shaping replaces gravity with an artificial task-potential the contact can pump into. Certifying with the natural mechanical energy and a dissipative fallback is the key move (309→42, ~7×), since the contact is passive with respect to that energy rather than the artificial task-potential energy-shaping introduces. A contact-anticipating barrier (a control-barrier on the distance-to-surface, capping approach velocity before compression) and more control authority take it further — 42 → 39 → 10/6000, ~30× from the naive certificate. What the last ~0.17% reveals is the floor: a torque-authority sweep shows the residual is mostly a controllability limit — with weak motors the fallback cannot arrest the elastic bounce, so the safe set is not control-invariant and no gate reaches zero; more torque recovers most of it (39→10) and then plateaus at a one-step-discretization floor. So energy-storing contact is certified to ~0.17% given the natural passive energy, an approach-anticipating barrier, and adequate control authority — and certifying that authority margin, the discretization, and contact-force / manipulation-task objectives is the remaining, now precisely-mapped frontier. Not a failure of energy-as-certificate; a measured map of exactly what it takes. This is a validity probe of a mechanism, not a benchmark of a system, and no comparison to any other institution is intended.

7 · The scoreboard — joules per viability-second

A certificate needs a metric the field lacks. J/VT — joules per viability-second held under disturbance — makes agency a number: run a body under an adversary trying to drive it out of the viable set, and measure the energy it spends to stay in against the time it stays viable. On the verified arm a puppet that commits the policy holds viability 26% at 347 W; the agent (certificate-gated) holds 100% at 57 W — cheaper and safer, not a trade — and a quiet body holds it for near-free (0.47 W). The verdict travels across bodies on the one scoreboard: on the real SO-101 the agent runs 0.25 W with 0 crashes against a single-vector puppet's 7.47 W and 36 crashes; the underactuated sweep (acrobot, hopper, humanoid) and the contact regimes all report here, the energy-storing frontier showing up as a priced penalty rather than a footnote.

Under it sits a thermodynamic floor. Viability is exactly the level set $\{V\le c\}$ held forward-invariant, so $V$ is the sufficient statistic for viability — measured: given $V$, the full state adds ~0 viability information. By Still, Sivak, Bell & Crooks, every bit a memory keeps beyond $V$ is non-predictive of viability — nostalgia, a strictly higher dissipation floor. The certificate keeps ~7 bits; a pixel world-model keeps $\sim\!10^5$, some $10^4$× more, almost all non-predictive of whether the body stays alive. That is the thermodynamic case for energy-as-certificate over model-the-whole-world. (J/VT is measured; the floor's bit-counts are order-of-magnitude and the tight non-equilibrium equality is a theory target, not yet a result.)

8 · Tying in reality — observability, not fidelity

Every certificate above is verified on the twin using the twin's own dynamics as oracle — which certifies the simulator, not the robot. Closing that gap surfaces an inversion. The discrete-barrier gate re-measures the real state each step and only predicts one step ahead, so its veto buffer absorbs a ±30% dynamics mismatch for free — motor gain, friction, mass. Dynamics fidelity is not the binding constraint. What bites is systematic bias and observability: a one-sided sensing error the buffer cannot average out (a miscalibrated velocity under-read) makes a naive gate leak; sizing the margin to the worst-case bias bound restores the guarantee. And when perception degrades, a fixed margin keeps trusting a state it can no longer see and runs the body reckless-fast, while an observability-aware margin recognizes it cannot see and gives up ~23% speed to stay safe — slower but safe. So for an energy certificate, sim-to-real is an observability problem, not a dynamics-rendering one. The raw-sensor→state-confidence pipeline is the real-perception frontier: the certificate side is what this closes; the perception side is the open work.

References & lineage

Chang, Roohi & Gao, Neural Lyapunov Control, NeurIPS 2019; Gao, Kong & Clarke, dReal: an SMT solver for nonlinear theories over the reals, CADE 2013 — the counterexample-guided synthesis and δ-complete verifier the learned certificate builds on.
This program's certificate toolchain (piecewise-linear → analytical-nonlinear → SMT-learned-ternary → 4D → SOS-to-8D, fixed-control) and its §5 law: a learned energy certifies strictly more than a quadratic only where the region of attraction is non-convex — here carried into the self-controlled unification.
Companion positioning paper: Energy Is the Certificate — the unclaimed intersection, Charlot Lab.

The reproducible probe scripts (the sound Taylor+CROWN verifiers, the direct-CLF and CEGIS synthesis, the dReal self-controlled worker) and the certified energies are the Institute's on-device research record. The formal whitepaper is the final deliverable and follows.