correctness: carry ranked countermodels for failed KLM queries

[SMC17]

Problem

KLM rational-closure rankings and Boolean/level query results replay exactly, but a failed query does not yet carry a concrete model at the decisive rank. The museum therefore correctly keeps KLM catalog-only.

Required result

Introduce an owned query decision that preserves entailed, decisive rank, active rule set, and a complete countermodel for non-entailment. No SAT unknown may be translated into exceptionality or a negative answer.

Acceptance gates

• Validate ranking length, rank range, and exact ranking before query replay.
• Non-entailment always contains a model satisfying background, active materialization, antecedent, and negated consequent.
• The checker verifies the model and decisive-rank minimality without trusting the producer Boolean.
• Entailment checks every required rank conclusively.
• Mutation tests corrupt rank, active rules, assignment, antecedent, and consequent.
• Exhaustive small-KB comparison against an independent ranked-model oracle.
• Formal exhibit specification documents the finite propositional cube fragment and limits.
• Promotion occurs only after all gates pass.