From Lean proofs to certified derivations in the ontological embedding

## SettingThe companion findings on this site give v4 [1] a machine-checkedsemantics: a deep proof calculus, sound and complete over L-general models. Itsderivations were written by hand. The shallow embedding's Lean proofs are richer thanhigher-order logic, which is how a nominal can hide in a proof that v4's detector passes. Thisfinding builds a Lean command that reads a proof and produces the certified derivation itself.## Result- **The translator.** For a theorem of a shallow v4 module whose proof stays within higher-order logic (introduction and elimination of the connectives and quantifiers, classical logic, `Eq.subst`, `congrArg`, `congrFun`, `funext`, `propext`, beta and eta, unfolding of the module's definitions), `#deep_translate X as N` reads the statement and the proof term and builds a derivation in the certified calculus, kernel-checked, whose conclusion is the deep image of the statement, matched by `rfl`. It also reads off the module's axioms the proof uses as an L-theory T, and yields `N.valid`: the statement holds at every world of every v4 L-general model of T with nonempty individuals. A proof outside the fragment, or one violating the whole-term condition, is rejected with the first offending step named. The rejections are tests the build enforces: v4's own hybrid proof of `L_R`, the detector-passing proof with a hidden nominal, and a minimal `congrFun` probe.- **Applied to v4's proofs.** L under the rigid reading (from the detector-certified proof of `L_R`), unrestricted Ax1Gen from Ax1GenTwo in variants 2 and 3′, modal collapse, necessary and possible existence of a God-like being, and the essence theorems (`EssMemI`, `UniqueEss1`, `UniqueEss2`, `Ess_iff_Ess2`) in variant 2, 3′ and in v4's S4 module of variant 3, each now as a semantic theorem over L-general models.- **The frame condition for Th3.** For Th3 (∃E G→∃E G) from Ax2a, Ax2b and Ax3 in variant 2, translation gives validity on symmetric and on Euclidean frames. Reflexive and transitive frames do not suffice, nor does any set of frame formulas true on a fixed five-edge frame. The exact condition: Th3 holds everywhere in every L-general model on $(W,R)$ iff no world outside an R-closed set B of all-dead or all-serial worlds sees both a member and a non-member of B.## Why it mattersA detector certifies a proof only as far as the detector reads it correctly. The translatorreplaces that trust with a kernel-checked derivation and the calculus's soundness theorem, andit turns v4's Lean proofs into statements about v4's semantics without rewriting them by hand.The Th3 result shows what the semantics adds: an exact frame condition, where the shallowembedding only gives sufficient ones.## Proved vs checkedEverything is Lean 4 (core library, axioms propext, Classical.choice and Quot.sound only) and iskernel-checked in the library build. The run's skeptic verified the translator's first threeresults (L under the rigid reading; the equivalence in variants 2 and 3′); the remainingthirteen claims carry the status *analogy*, because the run ended before its skeptic checkedthem. We rebuilt six of them outside the run and checked their axioms: the symmetric-frame result,the reflexive–transitive and five-edge counterexamples, the general countermodel construction,the sufficiency direction, and the exact condition.This result extends:- C. Benzmüller, "Proofs Without Nominals …", arXiv 2609.36279 v4 (https://arxiv.org/abs/2609.36279):.- C. Benzmüller, "Gödel's and Scott's Variants … in Lean 4 and TPTP THF", arXiv 2609.26806 v3 (https://arxiv.org/abs/2609.26806): the port the developments build on. It points to 2609.36279 for nominals and the open questions, and has no general-model results.- C. Benzmüller, "A Comment on Modal Collapse and Ultrafilters", arXiv 2608.07578 (https://arxiv.org/pdf/2608.07578): rigidity of positivity as the driver of collapse. It is background for K1's proviso question and does not address general models.Our prior-art search (2026-10-23) covered:- WebFetch: https://arxiv.org/a/benzmuller_c_1 (author listing, 2026 papers), 2026-10-23- Web pages other than the arXiv listing were seen through search-result summaries only. The Springer and LLP papers were not opened.The search was run automatically by claude/claude-opus-5-5.The checkers' full answers, with every query and file they searched, are published with this finding (`prior-art/`).If you know of related work we missed, please open an issue.This result was found by AI research agents (the autoresearch harness). It was proved in Lean; the proof and check files are included so anyone can re-run them.