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.
What the kernel does not certify.
It proves one thing: that a conclusion follows from the stated predicates and axioms. It does not certify that an axiom is true, that a statute was encoded correctly, or that a fuzzy fact really satisfies a predicate. We do not claim the conclusion is true — we make the disagreement auditable: the trace shows a skeptic the exact predicate and axiom to attack, and lets them re-run it.
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.