-- Reproduction axiom trail -- re-derived from source (TOOLCHAIN tier).
-- theorem : kalman_recursive_mmse
-- source  : machlib module MachLib.KalmanRecursive (proven directly, not emitted)
-- tool    : machlib d6d130a1 . lean via lake
-- when    : 2026-07-27T07:09:17Z
-- verdict : CLEAN -- sorryAx-free
-- forbid  : sorryAx  (cites Classical.choice via mach_mpoly)
-- (re-derive: make verify-proof)
--
'MachLib.Real.kalman_recursive_mmse' depends on axioms: [propext,
 Classical.choice,
 MachLib.Real,
 Quot.sound,
 MachLib.Real.addR,
 MachLib.Real.add_assoc,
 MachLib.Real.add_comm,
 MachLib.Real.add_lt_add_left,
 MachLib.Real.add_neg,
 MachLib.Real.add_zero,
 MachLib.Real.divR,
 MachLib.Real.leR,
 MachLib.Real.le_iff_lt_or_eq,
 MachLib.Real.ltR,
 MachLib.Real.lt_total,
 MachLib.Real.lt_trans_ax,
 MachLib.Real.mulR,
 MachLib.Real.mul_comm,
 MachLib.Real.mul_distrib,
 MachLib.Real.mul_pos,
 MachLib.Real.negR,
 MachLib.Real.subR,
 MachLib.Real.zeroR]