IndisputableMonolith.Verification.CPMBridge.Exports

   1import Mathlib
   2import IndisputableMonolith.Verification.CPMBridge.Initiality
   3
   4/-!
   5# CPM ⇒ RS (Paper Exports Without Exclusivity)
   6
   7This module re-exports the CPM universality corollary needed for paper
   8citation without importing the exclusivity adapter (and thus avoids
   9import cycles). It depends only on the Initiality scaffold.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Verification
  14namespace CPMBridge
  15namespace Exports
  16
  17open IndisputableMonolith.Verification.CPMBridge.Initiality
  18
  19abbrev matchesRSCore := Initiality.matchesRSCore
  20
  21theorem universality_implies_RS_core
  22  (U : Universality)
  23  (h : matchesRSCore U.Hodge.C ∧ matchesRSCore U.RH.C ∧ matchesRSCore U.NS.C ∧ matchesRSCore U.Goldbach.C) :
  24  matchesRSCore RS_sig.C :=
  25  Initiality.universality_implies_RS_core U h
  26
  27end Exports
  28end CPMBridge
  29end Verification
  30end IndisputableMonolith
  31