feat: add bounded symbolic guard reasoning to state/verify

[joshua-temple]

Adds bounded symbolic guard reasoning over the kernel's Core GuardNode tree, in a new stdlib-only state/verify/symbolic sub-package. Satisfiable reports whether a guard can ever hold, Contradiction whether it is provably dead (unsatisfiable), and Disjoint whether two guards are provably mutually exclusive (the basis for competing-transition / nondeterminism detection). The analyzer normalizes a guard to disjunctive normal form (pushing negation via De Morgan) and checks each conjunctive clause for a per-field contradiction — numeric fields as intervals (bounds, ne-exclusion), discrete string/bool/enum fields as value sets (eq/ne/in). It is a pure-Go bounded analyzer, not an SMT solver and no CGo: it is deliberately conservative, so a Rich or named-leaf guard, a cross-field comparison, or a duration/time field is treated as an unconstrained unknown — Contradiction and Disjoint are sound (a true verdict is always correct; unprovable cases are reported satisfiable / not-disjoint). It reads only the kernel's own GuardNode/ContextSchema, adding no dependency. (Overlaps — the whole-machine competing-transition scan built on Disjoint — follows next.) Additive; stdlib-only.