Proved Controller

A PID controller drives a plant to a moving setpoint. Its control output is computed three ways: the exact real, the rounded float a chip actually computes, and the machine-checked error band around the exact value. The float never leaves the band — that is Certcom.pid_grounded, watchable.

— exact real• float (rounded)▉ proved band (absErr)control output tanh(Kp·e + Ki·i + Kd·d)

Precision6-bitu = 0.0156

Float drift0actual |float − exact|

Proved bound0absErr ≥ drift

Inside band0/0✓ always

Tracking error0.000|setpoint − plant|

Kp1.50Ki0.40Kd0.05Precision6b

Drop the precision to 3–5 bits and the coral float scatters — but it stays inside the green band every frame. The band is the proved worst case (absErr, folded over Kp·e + Ki·i + Kd·d exactly as AbsoluteFold.lean does); the float is the actual rounded datapath (the FPBridge model, each op within u). Re-derivable: make verify-grounding in forge/reproduce.