IndisputableMonolith.NumberTheory.RSPhysicalThesisFromRCL

   1import IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition
   2
   3/-!
   4# RSPhysicalThesis From RCL Data
   5
   6Assembly layer: the old thesis follows from the decomposed RCL ledger data.
   7-/
   8
   9namespace IndisputableMonolith
  10namespace NumberTheory
  11
  12/-- Boundary transport plus the proved RCL/RH infrastructure implies the old
  13`RSPhysicalThesis`. -/
  14theorem rsPhysicalThesis_from_boundaryTransport (boundary : BoundaryTransportCert) :
  15    RSPhysicalThesis :=
  16  rsPhysicalThesis_of_data (rsPhysicalThesisData_of_boundaryTransport boundary)
  17
  18end NumberTheory
  19end IndisputableMonolith
  20