Function transpile 

pub fn transpile(ctx: &mut CodegenContext) -> ProjectOutput

Transpile an Aver program to a Lean 4 project.

Takes &mut ctx so it can run ctx.refresh_facts() upfront — keeps the derived sets (mutual_tco_members, recursive_fns) in sync with the current items + modules. Idempotent: production callers go through build_context which already populated them, so refresh recomputes the same answer; test stubs that build the ctx piecewise (push items in-place, bypass build_context) get the fresh sets they need.