Vi rapporterar om den formella verifieringsstatusen för de tio "bevisförpliktelserna" från det preliminära manuskriptet intitulerat "NIST SUCKS," tillsammans med en fullständig konstruktiv formalisering av ephemeralisekeringsramverket och den beskurna ruliadsamplingskonstructionen. Med hjälp av Lean 4 bevisassistenten (v4.28.0) tillsammans med Mathlib-biblioteket finner vi att Teorem 1 är formellt motbevisad—dess konjunktion innehåller subklausuler som är bevisligen falska inom typteori. Teoremerna 2–10 kan inte typkontrolleras eftersom de refererar till dussintals odefinierade identifierare. På den konstruktiva sidan tillhandahåller vi fyra kompletta, sorry-fria Lean 4-formaliseringar: (1) EphemeralSecurity.lean—ett kärnsekeringsramverk med nyckelephemeralitet, XOR-krypteringsriktighet, framåtsekretess, och deterministisk universumgenerering; (2) RuliadSampling.lean—en beskriven ruliaders konstruktion med PRF-baserade omöjlighetsbevis som visar att den beskurna enkla-stegs-utmatningen är beräkningsmässigt omöjlig att skilja från det fullständiga flervägssystemet; (3) QuantumEphemeralSecurity.lean—ett kvantumsynkroniserat universumcyklingramverk med XOR-injektivitet, frömöjling motståndskraft, framåtsekretess, och krypteringsriktighet; (4) RuliadUniversalProof.lean—en fullständig formalisering av beräkningsmässig irreducibilitet för XOR-baserad evolution, inklusive känslighet, propagation, en frågegräns, en ingen-enhetlig-genväg-teorem (diagonalargument), och huvudsäkerhetsteomet. Alla formella resultat är maskinverifierade, fria från sorry, och beror endast på standardaxiomen (propext, Classical.choice, Quot.sound).