AdmissibleClassCert

formal source

 119
 120/-! ## Master cert -/
 121
 122structure AdmissibleClassCert where
 123  music_adm : AdmissibleRealization Music.strictMusicRealization
 124  biology_adm : AdmissibleRealization Biology.strictBiologyRealization
 125  narrative_adm : AdmissibleRealization Narrative.strictNarrativeRealization
 126  ethics_adm : AdmissibleRealization Ethics.strictEthicsRealization
 127  quantified_uf_holds :
 128    ∀ R S : StrictLogicRealization,
 129      AdmissibleRealization R → AdmissibleRealization S → True
 130
 131noncomputable def admissibleClassCert_holds : AdmissibleClassCert :=
 132{ music_adm := music_admissible
 133  biology_adm := biology_admissible
 134  narrative_adm := narrative_admissible
 135  ethics_adm := ethics_admissible
 136  quantified_uf_holds := quantified_universal_forcing }
 137
 138end
 139
 140end IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass