Manuscript Hawk04-D@1 · Hawk04-D-v1.tex · section · 39b16f67
Enter, discard, and finite soundness
Complete interfaces and the finite operational core › Enter, discard, and finite soundness · lines 520–526
The theorem neither compiles the constants over a fixed gate library nor proves a physical endpoint. It uses the finite ownership discipline of Hawk04-B/C and the separate sequential-accounting comparison in En02-C CheungHawk04B,CheungHawk04C,CheungEn02C.