-- trail: kalman_variance_recursion_fixed_point
-- theorem: MachLib.Real.kalman_variance_recursion_fixed_point
-- source: machlib module (proven directly, not emitted)
-- machlib: b8d04bd6
-- rederived: 2026-07-26T21:25:34Z
-- verdict: CLEAN (sorryAx-free)
-- note: cites Classical.choice (via mach_mpoly / Real base) — forbid=sorryAx only

'MachLib.Real.kalman_variance_recursion_fixed_point' 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.div_def,
 MachLib.Real.leR,
 MachLib.Real.le_iff_lt_or_eq,
 MachLib.Real.ltR,
 MachLib.Real.lt_irrefl_ax,
 MachLib.Real.lt_total,
 MachLib.Real.lt_trans_ax,
 MachLib.Real.mulR,
 MachLib.Real.mul_assoc,
 MachLib.Real.mul_comm,
 MachLib.Real.mul_distrib,
 MachLib.Real.mul_inv,
 MachLib.Real.mul_lt_mul_of_pos_right,
 MachLib.Real.mul_one_ax,
 MachLib.Real.mul_pos,
 MachLib.Real.negR,
 MachLib.Real.oneR,
 MachLib.Real.one_div_pos_of_pos,
 MachLib.Real.subR,
 MachLib.Real.sub_def,
 MachLib.Real.zeroR,
 MachLib.Real.zero_lt_one_ax]