Function lower_transition_ir 

pub fn lower_transition_ir(
    tr: &Transition,
    state_ty: TyId,
    program: &CheckedProgram,
) -> IrPredicate

P6.8 ([DECISION A]/[DECISION E], #1165): lower a step invariant (Transition) into a real IrPredicate — seeds old/new, both bound to the agent’s own synthetic state-record type, exactly as checker::check_transitions does. state_ty is a parameter, not re-derived, for the same reason lower_invariant_ir’s own store_cells is: no persisted “this agent’s state type” table survives past check_agent_decls’s own transient scope. Called once per agent’s own transition list, by the same future caller lower_invariant_ir names.