tlm_p3_gate xtime reduces on the wrong bits (wrong for 87.6% of inputs, fails FIPS-197 vector DB135345); testbenches carry wrong expected values or report PASSED unconditionally; Lean files do not compile; Grover oracle is a placeholder. Claims of FIPS-197 compliance, testing and formal verification are withdrawn.