The tableau engine read bottom-up is a cut-free sequent calculus; cut on the covering pair \(\{ T\} ,\{ F,Z\} \) is admissible (semantic cut elimination on top of the engine certificate), weakening admissible, identity derivable.

The \(\gamma /\delta \) parameter rules carry the sign discipline to arbitrary domains (fresh witnesses exactly where the weak signs live); soundness measured (\(13/13\) verdicts cross-checked, open branches yield verified countermodels), completeness by Hintikka saturation (argued); undecidability via the J-guard embedding of classical FO. Lean port on the roadmap.

Finite-domain quantifiers are strict folds in the certified language (a singleton domain collapses both to the \(J_T\) guard); the \(n\)-ary signed rules are preimage-coverage theorems; UI/EG hold in membership form; eight battery verdicts are kernel evaluations of the certified engine.