We study how high-stakes AI can preserve evidence, expose assumptions, and make structured reasoning machine-checkable without pretending that uncertainty has disappeared.
Introduces a hybrid AI + Lean 4 architecture for patent analysis. The DAG coverage core is machine-verified once bounded match scores are fixed. Other analyses have separately disclosed verification statuses. Semantic inputs remain below the trust boundary; the case study is synthetic; adjudicated-case validation is identified as future work.
Develops assurance ideas for retrieval stability, support and contradiction, and tool-action gating. The goal is to let systems accept, narrow, request more evidence, or abstain based on explicit assurance signals.
A practical framework for evidence, trust boundaries, human ownership, and honest status labels as AI increases the volume and complexity of research work.
Compiled and accepted by the named checker, with disclosed axioms and environment.
Implemented and tested under stated conditions, but not a production or validation claim.
Defined in a paper or design, not yet compiled or deployed.
Evaluation protocol disclosed; results not yet claimed.
Not represented as a current product capability.