Round-six lemma `eval_le_mg`
ProvedJ6Seg.PreT.eval_le_mgAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPre1):
theorem J6Seg.PreT.eval_le_mg (s : IState HS) (V : Fin HS → ℕ) :
∀ e : Ex HS, (∀ i ∈ e.regs, |s.top i| ≤ V i) → |e.eval s| ≤ mg V e
Context. B-line IL, pre-tables (B5), part 1: magnitude bounds for register expressions
mg V e: a crude magnitude bound of the expression e when every register i it reads holds a
value of absolute value ≤ V i. It dominates every subterm, so mg V e < 2^B gives e.Bnd s B
(bnd_of_mg): the cost bounds of all pushes/assignments of the pre-table programs reduce to one
numeric inequality per expression.
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs65 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.PreT open IntMul NLogN NLogN.KIL
theorem J6Seg.PreT.eval_le_mg (s : IState HS) (V : Fin HS → ℕ) :
∀ e : Ex HS, (∀ i ∈ e.regs, |s.top i| ≤ V i) → |e.eval s| ≤ mg V e := by sorry