Configured reduction schedules

Decoding commutes with a reduction that rounds at every addition, independently of the storage plan. Nearest-even finite executions inherit the model's half-ULP error budget. These theorems are separate from the configured round-once collection API.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_eval_tree {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (t : Numerics.ReductionTree (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (Numerics.ReductionTree.eval (fun (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) => add x y rounding) id t) = Numerics.ReductionTree.eval (Formats.BinaryInterchange.Model.addWithRounding rounding) id (Numerics.ReductionTree.map toModel t)

Decoding preserves the entire schedule and its chosen rounding mode.

theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_eval_tree_sub_sum_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (t : Numerics.ReductionTree (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (hformat : format.isIEEE = true) (hfinite : Formats.BinaryInterchange.Model.ReductionTree.FiniteEval (Numerics.ReductionTree.map toModel t)) : |(toModel (Numerics.ReductionTree.eval (fun (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) => add x y Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) id t)).toReal - (List.map (Formats.BinaryInterchange.Model.toReal ∘ toModel) t.leaves).sum| ≤ Formats.BinaryInterchange.Model.ReductionTree.errorBudget (Numerics.ReductionTree.map toModel t)

Configured nearest-even execution inherits the finite model's absolute error enclosure.