1. Overview: from a user target to a Lean certificate
ASPBE begins with either a normalized target state or an operator together with its access model. It does not identify a plausible circuit with a proof. The library separates the requested mathematical object, a candidate implementation, the semantic proof, and the resource record.