Round-six lemma `fcost_sim`
ProvedNLogN.KFD.fcost_simAn 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.KFDBase):
theorem NLogN.KFD.fcost_sim {π : KIL.PMap} (hπ : KIL.PLow π) {p p' : RS} (h : KIL.RSim π p p') :
(∀ i v, π i = some v → i ∉ p.writes) → ∀ s, KIL.PV π s → p.ok s →
fcost p' s ≤ 200 * fcost p s
Context. KFD base: fine compilation of register programs
The register programs RS of KIL1–KIL6 are compiled by RS.code, whose counted loop
rep i n b keeps a binary counter on i and decrements it in every iteration (cost
Θ(zsz n) per iteration). fcode compiles the same program with a unary counter instead:
rep i n b ↦ push i n; toUL i i; loop i isMk (unmark i; fcode b); drop i
(the value n stays below the n marks as a sentinel; toUL is the linear binary → unary
conversion of KFCUnary). Everything else is compiled as by RS.code.
fcode_runs (simulation): if p.ok s and every loop body leaves its counter alone
(FOK p: the counter is not touched — read or written — by the body, and avoids the
toUL scratch stacks 26 … 29), then fcode p realises p.run with the cost fcost p s.
The run is proved relative to a set of ghost stacks (the counters of the enclosing loops,
which hold marks in the fine run and the binary count in the RS semantics).
fcost_le_cost: fcost p s ≤ 100 · p.cost s (coarse transfer of every KIL cost bound).
The point of fcost is the loop: per iteration it charges fcost b + 31 plus the amortised
toUL cost, i.e. O(1) overhead per iteration, independent of the size of the count.
FSp p s t c is the fine analogue of KIL.Sp.
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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFD
open IntMul NLogN.RS
open NLogN.KFC (marks marks_zero isMk NM toUL cUL uK uR uY uB)
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
theorem NLogN.KFD.fcost_sim {π : KIL.PMap} (hπ : KIL.PLow π) {p p' : RS} (h : KIL.RSim π p p') :
(∀ i v, π i = some v → i ∉ p.writes) → ∀ s, KIL.PV π s → p.ok s →
fcost p' s ≤ 200 * fcost p s := by sorry