HvdH machine lemma swapsPerm_fixHi (Relocating register programs)
ProvedNLogN.swapsPerm_fixHiThe following holds (Lean statement, in the scope of module NLogN.HRenRM):
theorem NLogN.swapsPerm_fixHi (l : List (Fin HS × Fin HS)) (h : swapsLow l = true) :
FixHi (swapsPerm l)
Context. The lemma belongs to the part Relocating register programs: For a permutation σ of the HS stacks fixing every stack ≥ 55 (the multiplication argument
55 and the expression scratch 56..63), Ex.ren σ, RS.ren σ, RM.ren σ rename every register
i to σ i. On the relocated state IState.rn σ s (stack σ i holds the old stack i) the
renamed program computes the relocated result, with the same side conditions and the same cost.
Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of .
-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.
import Definitions.Def_IntMul_HvdH_M_Defs8
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
set_option linter.unusedSimpArgs false
open NLogN
open IntMul
variable (σ : Equiv.Perm (Fin HS))
variable {σ}
theorem NLogN.swapsPerm_fixHi (l : List (Fin HS × Fin HS)) (h : swapsLow l = true) :
FixHi (swapsPerm l) := by sorry