4.9. Ce que chaque preuve ouverte y puise🔗

Cette section n'a pas de valeur propre ; elle en a par ce qu'elle rend possible, et la traçabilité doit être explicite pour que son achèvement soit mesurable.

Cette section a été écrite quand les trois preuves attendaient ; elle dit maintenant ce qu'elles ont pris. La préservation du typage par la traduction (chapitre 4, théorème 45) est planifiée (§4.7.6), non conduite. Ses trois premiers groupes se réduisent au lemme de commutation, et ses quatre cas résistants au foncteur d'effacement, le système de sortes, et l'appareil de ré-invocation bornée que les deux derniers partagent. La non-interférence graduée (théorème 13) est démontrée sur le fragment sans communication, temps compris (§4.7.3) ; son extension attend le même système de sortes. La divulgation délimitée (théorème 10) est démontrée sous la même réserve, la relation étant celle-là même requantifiée. Cette réserve est précisée depuis le §4.8 : le système de sortes rend la clause de session définissable, de sorte que les trois preuves s'étendent en principe à la strate qu'elles laissaient ; l'extension n'est pas conduite. Les trois reposent sur le lemme de substitution et sur la loi de cohérence qu'il a réclamée. Les règles de la loi distributive graduée et celles de la gradation indexée sont des règles, et appartiennent au jeu de règles du §3.6 dès qu'elles seront écrites.

Un dernier point inverse l'ordre apparent des priorités. Le métalangage du chapitre 4, qui est la cible de la traduction, est formellement présenté — grammaire, motifs, coupure — quand K7PL, qui en est la source, ne l'est pas. Cette asymétrie est le vrai retard de ce document, et cette section est ce qui la comble.