5.2. Least Fixed Points🔗

Cslib.Logic.FO.LFP.RawFormula is syntax whose formation conditions have not yet been checked. Cslib.Logic.FO.LFP.Formula packages that syntax with a proof of well-formedness. The lfp constructor binds a relation and a tuple of the same arity; its body must contain its own relation positively. Ordinary negation outside that recursion is allowed, as are nested fixed points and free parameters.

Raw semantics is total: it intersects all pre-fixed relations. The fixed-point unfolding and leastness laws require the positivity certificate. This distinction prevents a negative recursive body from silently acquiring the laws of a monotone least fixed point. fo_wf [definitions] checks formation of explicit syntax by unfolding its named formulas and the syntactic checks.

For a finite structure with n elements and an arity-k relation, iteration starts at the empty relation and reaches the least fixed point by stage n ^ k. The theorem proves equality at that stage, including empty domains and arity zero; it counts possible tuples, rather than all possible relations. OrderHom.iterate_card_bot_eq_lfp provides the underlying general powerset bound. The native model checker uses this bound and charges for constructing and reading its relation tables. Its polynomial-time certificate covers arbitrary fixed formulas, including nested fixed points and captured parameters.