Prove2Me

KRF.universal_iff_reducibleTheta

Proved
KRF.universal_iff_reducibleTheta

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

A formalism is universal iff it reduces the canonical (universal) one — the paper's corollary.

Preamble
import Definitions.Def_KRF_Data
import Definitions.Def_KRF_Machinery
import Definitions.Def_KRF_RenamingProps
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ σ : Sig}
Formal statement
theorem KRF.universal_iff_reducibleTheta {σD σQ : Sig} {Q : QueryLanguage σQ}
    (Θ Γ : Krf σD σQ Q) (hΘ : Universal Θ) :
    Universal Γ ↔ ReducibleTo Θ Γ :=
  sorry
Source
arXiv 2412.11855v2

View graph