Prove2Me

KRF.universalTheta

Open
KRF.universalTheta

by jario · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Main existence theorem (Theorem 1): a universal KRF exists (the canonical one).

Preamble
import Definitions.Def_KRF_Machinery
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ : Sig}
/-- The canonical-KRF predicate (platform form of thetaKrf): the theory
engine mapping carried by the StarContract. -/
def IsTheta {σD σQ : Sig} {Q : QueryLanguage σQ} (c : Coding σD σQ)
    (S : StarContract σD σQ Q) (T : Krf σD σQ Q) : Prop :=
  ∃ hdom : T.dom = S.isTheory,
    ∀ (π : Nat) (h : S.isTheory π), ∀ D φ,
      T.Γ π (hdom ▸ h) D φ ↔ KM (S.theoryEngine h) D φ
Formal statement
theorem KRF.universalTheta {Q : QueryLanguage σQ} (c : Coding σD σQ) (S : StarContract σD σQ Q) :
    ∃ T : Krf σD σQ Q, IsTheta c S T ∧ Universal T :=
  sorry
Source
arXiv 2412.11855v2 (Zhang, Jiang, Quan)

View graph