Comments
The realization theorem, Theorem 6.5, is formulated for the logic of proofs LP with the total constant specification containing c:A for each constant c and each axiom A. However, this requirement can be eased.
What we need from CS in this proof is to support the Lifting Lemma, Lemma 6.1, and substitutions..~,1,... 7,n,
i~ -.. the former requires axiomatically appropriate CS and the latter a schematic CS. So, a natural sufficient requirement for this proof of the realization theorem is axiomatically appropriate and schematic.
The realization algorithm given in the proof of Theorem 6.5 is in fact exponential in the length of a given cut-free derivation of S4, mostly because of the repeating use of the Lifting Lemma. A polynomial time realization algorithm was offered in Brezhnev and Kuznets (2006).
Some S4-theorems admit essentially different realizations in LP. For exam
a is a constant that realizes F → F. Again the second is simply a tautology.
This time the first formula involves in an essential way the operation “·”. 
however, was to keep its language reasonably general because the realization of S4 was not the Logic of Proofs' only intended application.