Module decide 

decide — proof by evaluation for closed decidable goals.

The router below is untrusted: it evaluates the goal with machine arithmetic and, only when the goal is TRUE, builds the derivation whose leaves re-derive that truth through certified channels — ArithDecision (the proof-producing arithmetic oracle) for ground Int identities, NativeDecide (the kernel’s trusted-evaluator route via the reduceBool hook and a Decidable instance) for ground comparisons and Bool equalities. Propositional structure recurses through the ordinary intro rules. A false, open, or unsupported goal yields None — decide declines, it never guesses.