Thesis
Why axiomatic agents.
LLMs are pattern matchers.
They are extraordinary at extraction, paraphrase, and association. They are also confidently wrong, untraceable, and bad at composition. We do not ask them to compose proofs.
Theorem provers don't read.
Lean4 will compose a verified proof from premises, but it cannot read a 47-page complaint or an OHLCV time series. It needs a structured input. We give it one.
Predicates are the bridge.
A predicate is a function from natural-language or numeric evidence to a Boolean. Each predicate is a small sub-agent with a narrow specification, an evidence quote, and an uncertainty score. The kernel reads only its Boolean; the human reads the evidence.
The kernel is the referee.
Lean composes the proof using axioms encoded from the statute or the evaluation framework. The proof is reproducible, exportable, and adversarially defensible.
Two domains, one method.
Qnarre points the kernel at legal complaints. Qresev points it at portfolios and securities. The shape of the system is identical; only the predicates and the axioms differ.