-- Reproduction axiom trail -- re-derived from source (TOOLCHAIN tier).
-- theorem : kalman2d_cov_predict_psd
-- source  : eml-stdlib/eml_stdlib/control/kalman2d_predict.eml  ->  eml-compile --target lean
-- tool    : forge 92b1b41 . machlib 2c8cc0c . lean via lake
-- when    : 2026-07-07T15:39:51Z
-- verdict : CLEAN -- footprint free of sorry- and classical-citation axioms
-- forbid  : sorryAx, Classical.choice
-- (re-derive: make verify-proof)
--
'kalman2d_cov_predict_psd' depends on axioms: [propext,
 MachLib.Real,
 Quot.sound,
 MachLib.Real.addR,
 MachLib.Real.add_assoc,
 MachLib.Real.add_comm,
 MachLib.Real.add_lt_add_left,
 MachLib.Real.add_zero,
 MachLib.Real.leR,
 MachLib.Real.le_iff_lt_or_eq,
 MachLib.Real.ltR,
 MachLib.Real.lt_trans_ax,
 MachLib.Real.mulR,
 MachLib.Real.mul_assoc,
 MachLib.Real.mul_comm,
 MachLib.Real.mul_distrib,
 MachLib.Real.zeroR]